| Metamath
Proof Explorer Theorem List (p. 216 of 494) | < Previous Next > | |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | pzriprnglem10 21501 | Lemma 10 for pzriprng 21508: The equivalence classes of 𝑅 modulo 𝐽. (Contributed by AV, 22-Mar-2025.) |
| ⊢ 𝑅 = (ℤring ×s ℤring) & ⊢ 𝐼 = (ℤ × {0}) & ⊢ 𝐽 = (𝑅 ↾s 𝐼) & ⊢ 1 = (1r‘𝐽) & ⊢ ∼ = (𝑅 ~QG 𝐼) ⇒ ⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → [〈𝑋, 𝑌〉] ∼ = (ℤ × {𝑌})) | ||
| Theorem | pzriprnglem11 21502* | Lemma 11 for pzriprng 21508: The base set of the quotient of 𝑅 and 𝐽. (Contributed by AV, 22-Mar-2025.) |
| ⊢ 𝑅 = (ℤring ×s ℤring) & ⊢ 𝐼 = (ℤ × {0}) & ⊢ 𝐽 = (𝑅 ↾s 𝐼) & ⊢ 1 = (1r‘𝐽) & ⊢ ∼ = (𝑅 ~QG 𝐼) & ⊢ 𝑄 = (𝑅 /s ∼ ) ⇒ ⊢ (Base‘𝑄) = ∪ 𝑟 ∈ ℤ {(ℤ × {𝑟})} | ||
| Theorem | pzriprnglem12 21503 | Lemma 12 for pzriprng 21508: 𝑄 has a ring unity. (Contributed by AV, 23-Mar-2025.) |
| ⊢ 𝑅 = (ℤring ×s ℤring) & ⊢ 𝐼 = (ℤ × {0}) & ⊢ 𝐽 = (𝑅 ↾s 𝐼) & ⊢ 1 = (1r‘𝐽) & ⊢ ∼ = (𝑅 ~QG 𝐼) & ⊢ 𝑄 = (𝑅 /s ∼ ) ⇒ ⊢ (𝑋 ∈ (Base‘𝑄) → (((ℤ × {1})(.r‘𝑄)𝑋) = 𝑋 ∧ (𝑋(.r‘𝑄)(ℤ × {1})) = 𝑋)) | ||
| Theorem | pzriprnglem13 21504 | Lemma 13 for pzriprng 21508: 𝑄 is a unital ring. (Contributed by AV, 23-Mar-2025.) |
| ⊢ 𝑅 = (ℤring ×s ℤring) & ⊢ 𝐼 = (ℤ × {0}) & ⊢ 𝐽 = (𝑅 ↾s 𝐼) & ⊢ 1 = (1r‘𝐽) & ⊢ ∼ = (𝑅 ~QG 𝐼) & ⊢ 𝑄 = (𝑅 /s ∼ ) ⇒ ⊢ 𝑄 ∈ Ring | ||
| Theorem | pzriprnglem14 21505 | Lemma 14 for pzriprng 21508: The ring unity of the ring 𝑄. (Contributed by AV, 23-Mar-2025.) |
| ⊢ 𝑅 = (ℤring ×s ℤring) & ⊢ 𝐼 = (ℤ × {0}) & ⊢ 𝐽 = (𝑅 ↾s 𝐼) & ⊢ 1 = (1r‘𝐽) & ⊢ ∼ = (𝑅 ~QG 𝐼) & ⊢ 𝑄 = (𝑅 /s ∼ ) ⇒ ⊢ (1r‘𝑄) = (ℤ × {1}) | ||
| Theorem | pzriprngALT 21506 | The non-unital ring (ℤring ×s ℤring) is unital because it has the two-sided ideal (ℤ × {0}), which is unital, and the quotient of the ring and the ideal is also unital (using ring2idlqusb 21320). (Contributed by AV, 23-Mar-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (ℤring ×s ℤring) ∈ Ring | ||
| Theorem | pzriprng1ALT 21507 | The ring unity of the ring (ℤring ×s ℤring) constructed from the ring unity of the two-sided ideal (ℤ × {0}) and the ring unity of the quotient of the ring and the ideal (using ring2idlqus1 21329). (Contributed by AV, 24-Mar-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (1r‘(ℤring ×s ℤring)) = 〈1, 1〉 | ||
| Theorem | pzriprng 21508 | The non-unital ring (ℤring ×s ℤring) is unital. Direct proof in contrast to pzriprngALT 21506. (Contributed by AV, 25-Mar-2025.) |
| ⊢ (ℤring ×s ℤring) ∈ Ring | ||
| Theorem | pzriprng1 21509 | The ring unity of the ring (ℤring ×s ℤring). Direct proof in contrast to pzriprng1ALT 21507. (Contributed by AV, 25-Mar-2025.) |
| ⊢ (1r‘(ℤring ×s ℤring)) = 〈1, 1〉 | ||
| Syntax | czrh 21510 | Map the rationals into a field, or the integers into a ring. |
| class ℤRHom | ||
| Syntax | czlm 21511 | Augment an abelian group with vector space operations to turn it into a ℤ-module. |
| class ℤMod | ||
| Syntax | cchr 21512 | Syntax for ring characteristic. |
| class chr | ||
| Syntax | czn 21513 | The ring of integers modulo 𝑛. |
| class ℤ/nℤ | ||
| Definition | df-zrh 21514 | Define the unique homomorphism from the integers into a ring. This encodes the usual notation of 𝑛 = 1r + 1r + ... + 1r for integers (see also df-mulg 19086). (Contributed by Mario Carneiro, 13-Jun-2015.) (Revised by AV, 12-Jun-2019.) |
| ⊢ ℤRHom = (𝑟 ∈ V ↦ ∪ (ℤring RingHom 𝑟)) | ||
| Definition | df-zlm 21515 | Augment an abelian group with vector space operations to turn it into a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 12-Jun-2019.) |
| ⊢ ℤMod = (𝑔 ∈ V ↦ ((𝑔 sSet 〈(Scalar‘ndx), ℤring〉) sSet 〈( ·𝑠 ‘ndx), (.g‘𝑔)〉)) | ||
| Definition | df-chr 21516 | The characteristic of a ring is the smallest positive integer which is equal to 0 when interpreted in the ring, or 0 if there is no such positive integer. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
| ⊢ chr = (𝑔 ∈ V ↦ ((od‘𝑔)‘(1r‘𝑔))) | ||
| Definition | df-zn 21517* | Define the ring of integers mod 𝑛. This is literally the quotient ring of ℤ by the ideal 𝑛ℤ, but we augment it with a total order. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 12-Jun-2019.) |
| ⊢ ℤ/nℤ = (𝑛 ∈ ℕ0 ↦ ⦋ℤring / 𝑧⦌⦋(𝑧 /s (𝑧 ~QG ((RSpan‘𝑧)‘{𝑛}))) / 𝑠⦌(𝑠 sSet 〈(le‘ndx), ⦋((ℤRHom‘𝑠) ↾ if(𝑛 = 0, ℤ, (0..^𝑛))) / 𝑓⦌((𝑓 ∘ ≤ ) ∘ ◡𝑓)〉)) | ||
| Theorem | zrhval 21518 | Define the unique homomorphism from the integers to a ring or field. (Contributed by Mario Carneiro, 13-Jun-2015.) (Revised by AV, 12-Jun-2019.) |
| ⊢ 𝐿 = (ℤRHom‘𝑅) ⇒ ⊢ 𝐿 = ∪ (ℤring RingHom 𝑅) | ||
| Theorem | zrhval2 21519* | Alternate value of the ℤRHom homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.) |
| ⊢ 𝐿 = (ℤRHom‘𝑅) & ⊢ · = (.g‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝐿 = (𝑛 ∈ ℤ ↦ (𝑛 · 1 ))) | ||
| Theorem | zrhmulg 21520 | Value of the ℤRHom homomorphism. (Contributed by Mario Carneiro, 14-Jun-2015.) |
| ⊢ 𝐿 = (ℤRHom‘𝑅) & ⊢ · = (.g‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ ℤ) → (𝐿‘𝑁) = (𝑁 · 1 )) | ||
| Theorem | zrhrhmb 21521 | The ℤRHom homomorphism is the unique ring homomorphism from ℤ. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 12-Jun-2019.) |
| ⊢ 𝐿 = (ℤRHom‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝐹 ∈ (ℤring RingHom 𝑅) ↔ 𝐹 = 𝐿)) | ||
| Theorem | zrhrhm 21522 | The ℤRHom homomorphism is a homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.) (Revised by AV, 12-Jun-2019.) |
| ⊢ 𝐿 = (ℤRHom‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝐿 ∈ (ℤring RingHom 𝑅)) | ||
| Theorem | zrh1 21523 | Interpretation of 1 in a ring. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
| ⊢ 𝐿 = (ℤRHom‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝐿‘1) = 1 ) | ||
| Theorem | zrh0 21524 | Interpretation of 0 in a ring. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
| ⊢ 𝐿 = (ℤRHom‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝐿‘0) = 0 ) | ||
| Theorem | zrhpropd 21525* | The ℤ ring homomorphism depends only on the ring attributes of a structure. (Contributed by Mario Carneiro, 15-Jun-2015.) |
| ⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦)) ⇒ ⊢ (𝜑 → (ℤRHom‘𝐾) = (ℤRHom‘𝐿)) | ||
| Theorem | zlmval 21526 | Augment an abelian group with vector space operations to turn it into a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 12-Jun-2019.) |
| ⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ · = (.g‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑉 → 𝑊 = ((𝐺 sSet 〈(Scalar‘ndx), ℤring〉) sSet 〈( ·𝑠 ‘ndx), · 〉)) | ||
| Theorem | zlmlem 21527 | Lemma for zlmbas 21529 and zlmplusg 21531. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.) |
| ⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ 𝐸 = Slot (𝐸‘ndx) & ⊢ (𝐸‘ndx) ≠ (Scalar‘ndx) & ⊢ (𝐸‘ndx) ≠ ( ·𝑠 ‘ndx) ⇒ ⊢ (𝐸‘𝐺) = (𝐸‘𝑊) | ||
| Theorem | zlmlemOLD 21528 | Obsolete version of zlmlem 21527 as of 3-Nov-2024. Lemma for zlmbas 21529 and zlmplusg 21531. (Contributed by Mario Carneiro, 2-Oct-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑁 < 5 ⇒ ⊢ (𝐸‘𝐺) = (𝐸‘𝑊) | ||
| Theorem | zlmbas 21529 | Base set of a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.) |
| ⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ 𝐵 = (Base‘𝑊) | ||
| Theorem | zlmbasOLD 21530 | Obsolete version of zlmbas 21529 as of 3-Nov-2024. Base set of a ℤ -module. (Contributed by Mario Carneiro, 2-Oct-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ 𝐵 = (Base‘𝑊) | ||
| Theorem | zlmplusg 21531 | Group operation of a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.) |
| ⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ + = (+g‘𝑊) | ||
| Theorem | zlmplusgOLD 21532 | Obsolete version of zlmbas 21529 as of 3-Nov-2024. Group operation of a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ + = (+g‘𝑊) | ||
| Theorem | zlmmulr 21533 | Ring operation of a ℤ-module (if present). (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.) |
| ⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ · = (.r‘𝐺) ⇒ ⊢ · = (.r‘𝑊) | ||
| Theorem | zlmmulrOLD 21534 | Obsolete version of zlmbas 21529 as of 3-Nov-2024. Ring operation of a ℤ-module (if present). (Contributed by Mario Carneiro, 2-Oct-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ · = (.r‘𝐺) ⇒ ⊢ · = (.r‘𝑊) | ||
| Theorem | zlmsca 21535 | Scalar ring of a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 12-Jun-2019.) (Proof shortened by AV, 2-Nov-2024.) |
| ⊢ 𝑊 = (ℤMod‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑉 → ℤring = (Scalar‘𝑊)) | ||
| Theorem | zlmvsca 21536 | Scalar multiplication operation of a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| ⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ · = (.g‘𝐺) ⇒ ⊢ · = ( ·𝑠 ‘𝑊) | ||
| Theorem | zlmlmod 21537 | The ℤ-module operation turns an arbitrary abelian group into a left module over ℤ. Also see zlmassa 21923. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| ⊢ 𝑊 = (ℤMod‘𝐺) ⇒ ⊢ (𝐺 ∈ Abel ↔ 𝑊 ∈ LMod) | ||
| Theorem | chrval 21538 | Definition substitution of the ring characteristic. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
| ⊢ 𝑂 = (od‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝐶 = (chr‘𝑅) ⇒ ⊢ (𝑂‘ 1 ) = 𝐶 | ||
| Theorem | chrcl 21539 | Closure of the characteristic. (Contributed by Mario Carneiro, 23-Sep-2015.) |
| ⊢ 𝐶 = (chr‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝐶 ∈ ℕ0) | ||
| Theorem | chrid 21540 | The canonical ℤ ring homomorphism applied to a ring's characteristic is zero. (Contributed by Mario Carneiro, 23-Sep-2015.) |
| ⊢ 𝐶 = (chr‘𝑅) & ⊢ 𝐿 = (ℤRHom‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝐿‘𝐶) = 0 ) | ||
| Theorem | chrdvds 21541 | The ℤ ring homomorphism is zero only at multiples of the characteristic. (Contributed by Mario Carneiro, 23-Sep-2015.) |
| ⊢ 𝐶 = (chr‘𝑅) & ⊢ 𝐿 = (ℤRHom‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ ℤ) → (𝐶 ∥ 𝑁 ↔ (𝐿‘𝑁) = 0 )) | ||
| Theorem | chrcong 21542 | If two integers are congruent relative to the ring characteristic, their images in the ring are the same. (Contributed by Mario Carneiro, 24-Sep-2015.) |
| ⊢ 𝐶 = (chr‘𝑅) & ⊢ 𝐿 = (ℤRHom‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐶 ∥ (𝑀 − 𝑁) ↔ (𝐿‘𝑀) = (𝐿‘𝑁))) | ||
| Theorem | dvdschrmulg 21543 | In a ring, any multiple of the characteristics annihilates all elements. (Contributed by Thierry Arnoux, 6-Sep-2016.) |
| ⊢ 𝐶 = (chr‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.g‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐶 ∥ 𝑁 ∧ 𝐴 ∈ 𝐵) → (𝑁 · 𝐴) = 0 ) | ||
| Theorem | fermltlchr 21544 | A generalization of Fermat's little theorem in a commutative ring 𝐹 of prime characteristic. See fermltl 16821. (Contributed by Thierry Arnoux, 9-Jan-2024.) |
| ⊢ 𝑃 = (chr‘𝐹) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ ↑ = (.g‘(mulGrp‘𝐹)) & ⊢ 𝐴 = ((ℤRHom‘𝐹)‘𝐸) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝐸 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ CRing) ⇒ ⊢ (𝜑 → (𝑃 ↑ 𝐴) = 𝐴) | ||
| Theorem | chrnzr 21545 | Nonzero rings are precisely those with characteristic not 1. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
| ⊢ (𝑅 ∈ Ring → (𝑅 ∈ NzRing ↔ (chr‘𝑅) ≠ 1)) | ||
| Theorem | chrrhm 21546 | The characteristic restriction on ring homomorphisms. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
| ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (chr‘𝑆) ∥ (chr‘𝑅)) | ||
| Theorem | domnchr 21547 | The characteristic of a domain can only be zero or a prime. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
| ⊢ (𝑅 ∈ Domn → ((chr‘𝑅) = 0 ∨ (chr‘𝑅) ∈ ℙ)) | ||
| Theorem | znlidl 21548 | The set 𝑛ℤ is an ideal in ℤ. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 13-Jun-2019.) |
| ⊢ 𝑆 = (RSpan‘ℤring) ⇒ ⊢ (𝑁 ∈ ℤ → (𝑆‘{𝑁}) ∈ (LIdeal‘ℤring)) | ||
| Theorem | zncrng2 21549 | Making a commutative ring as a quotient of ℤ and 𝑛ℤ. (Contributed by Mario Carneiro, 12-Jun-2015.) (Revised by AV, 13-Jun-2019.) |
| ⊢ 𝑆 = (RSpan‘ℤring) & ⊢ 𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁}))) ⇒ ⊢ (𝑁 ∈ ℤ → 𝑈 ∈ CRing) | ||
| Theorem | znval 21550 | The value of the ℤ/nℤ structure. It is defined as the quotient ring ℤ / 𝑛ℤ, with an "artificial" ordering added to make it a Toset. (In other words, ℤ/nℤ is a ring with an order , but it is not an ordered ring , which as a term implies that the order is compatible with the ring operations in some way.) (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by Mario Carneiro, 2-May-2016.) (Revised by AV, 13-Jun-2019.) |
| ⊢ 𝑆 = (RSpan‘ℤring) & ⊢ 𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁}))) & ⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝐹 = ((ℤRHom‘𝑈) ↾ 𝑊) & ⊢ 𝑊 = if(𝑁 = 0, ℤ, (0..^𝑁)) & ⊢ ≤ = ((𝐹 ∘ ≤ ) ∘ ◡𝐹) ⇒ ⊢ (𝑁 ∈ ℕ0 → 𝑌 = (𝑈 sSet 〈(le‘ndx), ≤ 〉)) | ||
| Theorem | znle 21551 | The value of the ℤ/nℤ structure. It is defined as the quotient ring ℤ / 𝑛ℤ, with an "artificial" ordering added to make it a Toset. (In other words, ℤ/nℤ is a ring with an order , but it is not an ordered ring , which as a term implies that the order is compatible with the ring operations in some way.) (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 13-Jun-2019.) |
| ⊢ 𝑆 = (RSpan‘ℤring) & ⊢ 𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁}))) & ⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝐹 = ((ℤRHom‘𝑈) ↾ 𝑊) & ⊢ 𝑊 = if(𝑁 = 0, ℤ, (0..^𝑁)) & ⊢ ≤ = (le‘𝑌) ⇒ ⊢ (𝑁 ∈ ℕ0 → ≤ = ((𝐹 ∘ ≤ ) ∘ ◡𝐹)) | ||
| Theorem | znval2 21552 | Self-referential expression for the ℤ/nℤ structure. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 13-Jun-2019.) |
| ⊢ 𝑆 = (RSpan‘ℤring) & ⊢ 𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁}))) & ⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ ≤ = (le‘𝑌) ⇒ ⊢ (𝑁 ∈ ℕ0 → 𝑌 = (𝑈 sSet 〈(le‘ndx), ≤ 〉)) | ||
| Theorem | znbaslem 21553 | Lemma for znbas 21562. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by Mario Carneiro, 14-Aug-2015.) (Revised by AV, 13-Jun-2019.) (Revised by AV, 9-Sep-2021.) (Revised by AV, 3-Nov-2024.) |
| ⊢ 𝑆 = (RSpan‘ℤring) & ⊢ 𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁}))) & ⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝐸 = Slot (𝐸‘ndx) & ⊢ (𝐸‘ndx) ≠ (le‘ndx) ⇒ ⊢ (𝑁 ∈ ℕ0 → (𝐸‘𝑈) = (𝐸‘𝑌)) | ||
| Theorem | znbaslemOLD 21554 | Obsolete version of znbaslem 21553 as of 3-Nov-2024. Lemma for znbas 21562. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by Mario Carneiro, 14-Aug-2015.) (Revised by AV, 13-Jun-2019.) (Revised by AV, 9-Sep-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝑆 = (RSpan‘ℤring) & ⊢ 𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁}))) & ⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝐸 = Slot 𝐾 & ⊢ 𝐾 ∈ ℕ & ⊢ 𝐾 < ;10 ⇒ ⊢ (𝑁 ∈ ℕ0 → (𝐸‘𝑈) = (𝐸‘𝑌)) | ||
| Theorem | znbas2 21555 | The base set of ℤ/nℤ is the same as the quotient ring it is based on. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) (Revised by AV, 3-Nov-2024.) |
| ⊢ 𝑆 = (RSpan‘ℤring) & ⊢ 𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁}))) & ⊢ 𝑌 = (ℤ/nℤ‘𝑁) ⇒ ⊢ (𝑁 ∈ ℕ0 → (Base‘𝑈) = (Base‘𝑌)) | ||
| Theorem | znbas2OLD 21556 | Obsolete version of znbas2 21555 as of 3-Nov-2024. The base set of ℤ/nℤ is the same as the quotient ring it is based on. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝑆 = (RSpan‘ℤring) & ⊢ 𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁}))) & ⊢ 𝑌 = (ℤ/nℤ‘𝑁) ⇒ ⊢ (𝑁 ∈ ℕ0 → (Base‘𝑈) = (Base‘𝑌)) | ||
| Theorem | znadd 21557 | The additive structure of ℤ/nℤ is the same as the quotient ring it is based on. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) (Revised by AV, 3-Nov-2024.) |
| ⊢ 𝑆 = (RSpan‘ℤring) & ⊢ 𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁}))) & ⊢ 𝑌 = (ℤ/nℤ‘𝑁) ⇒ ⊢ (𝑁 ∈ ℕ0 → (+g‘𝑈) = (+g‘𝑌)) | ||
| Theorem | znaddOLD 21558 | Obsolete version of znadd 21557 as of 3-Nov-2024. The additive structure of ℤ/nℤ is the same as the quotient ring it is based on. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝑆 = (RSpan‘ℤring) & ⊢ 𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁}))) & ⊢ 𝑌 = (ℤ/nℤ‘𝑁) ⇒ ⊢ (𝑁 ∈ ℕ0 → (+g‘𝑈) = (+g‘𝑌)) | ||
| Theorem | znmul 21559 | The multiplicative structure of ℤ/nℤ is the same as the quotient ring it is based on. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) (Revised by AV, 3-Nov-2024.) |
| ⊢ 𝑆 = (RSpan‘ℤring) & ⊢ 𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁}))) & ⊢ 𝑌 = (ℤ/nℤ‘𝑁) ⇒ ⊢ (𝑁 ∈ ℕ0 → (.r‘𝑈) = (.r‘𝑌)) | ||
| Theorem | znmulOLD 21560 | Obsolete version of znadd 21557 as of 3-Nov-2024. The multiplicative structure of ℤ/nℤ is the same as the quotient ring it is based on. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝑆 = (RSpan‘ℤring) & ⊢ 𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁}))) & ⊢ 𝑌 = (ℤ/nℤ‘𝑁) ⇒ ⊢ (𝑁 ∈ ℕ0 → (.r‘𝑈) = (.r‘𝑌)) | ||
| Theorem | znzrh 21561 | The ℤ ring homomorphism of ℤ/nℤ is inherited from the quotient ring it is based on. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 13-Jun-2019.) |
| ⊢ 𝑆 = (RSpan‘ℤring) & ⊢ 𝑈 = (ℤring /s (ℤring ~QG (𝑆‘{𝑁}))) & ⊢ 𝑌 = (ℤ/nℤ‘𝑁) ⇒ ⊢ (𝑁 ∈ ℕ0 → (ℤRHom‘𝑈) = (ℤRHom‘𝑌)) | ||
| Theorem | znbas 21562 | The base set of ℤ/nℤ structure. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) |
| ⊢ 𝑆 = (RSpan‘ℤring) & ⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝑅 = (ℤring ~QG (𝑆‘{𝑁})) ⇒ ⊢ (𝑁 ∈ ℕ0 → (ℤ / 𝑅) = (Base‘𝑌)) | ||
| Theorem | zncrng 21563 | ℤ/nℤ is a commutative ring. (Contributed by Mario Carneiro, 15-Jun-2015.) |
| ⊢ 𝑌 = (ℤ/nℤ‘𝑁) ⇒ ⊢ (𝑁 ∈ ℕ0 → 𝑌 ∈ CRing) | ||
| Theorem | znzrh2 21564* | The ℤ ring homomorphism maps elements to their equivalence classes. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) |
| ⊢ 𝑆 = (RSpan‘ℤring) & ⊢ ∼ = (ℤring ~QG (𝑆‘{𝑁})) & ⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑌) ⇒ ⊢ (𝑁 ∈ ℕ0 → 𝐿 = (𝑥 ∈ ℤ ↦ [𝑥] ∼ )) | ||
| Theorem | znzrhval 21565 | The ℤ ring homomorphism maps elements to their equivalence classes. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) |
| ⊢ 𝑆 = (RSpan‘ℤring) & ⊢ ∼ = (ℤring ~QG (𝑆‘{𝑁})) & ⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑌) ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) → (𝐿‘𝐴) = [𝐴] ∼ ) | ||
| Theorem | znzrhfo 21566 | The ℤ ring homomorphism is a surjection onto ℤ/nℤ. (Contributed by Mario Carneiro, 15-Jun-2015.) |
| ⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝐿 = (ℤRHom‘𝑌) ⇒ ⊢ (𝑁 ∈ ℕ0 → 𝐿:ℤ–onto→𝐵) | ||
| Theorem | zncyg 21567 | The group ℤ / 𝑛ℤ is cyclic for all 𝑛 (including 𝑛 = 0). (Contributed by Mario Carneiro, 21-Apr-2016.) |
| ⊢ 𝑌 = (ℤ/nℤ‘𝑁) ⇒ ⊢ (𝑁 ∈ ℕ0 → 𝑌 ∈ CycGrp) | ||
| Theorem | zndvds 21568 | Express equality of equivalence classes in ℤ / 𝑛ℤ in terms of divisibility. (Contributed by Mario Carneiro, 15-Jun-2015.) |
| ⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑌) ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐿‘𝐴) = (𝐿‘𝐵) ↔ 𝑁 ∥ (𝐴 − 𝐵))) | ||
| Theorem | zndvds0 21569 | Special case of zndvds 21568 when one argument is zero. (Contributed by Mario Carneiro, 15-Jun-2015.) |
| ⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑌) & ⊢ 0 = (0g‘𝑌) ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) → ((𝐿‘𝐴) = 0 ↔ 𝑁 ∥ 𝐴)) | ||
| Theorem | znf1o 21570 | The function 𝐹 enumerates all equivalence classes in ℤ/nℤ for each 𝑛. When 𝑛 = 0, ℤ / 0ℤ = ℤ / {0} ≈ ℤ so we let 𝑊 = ℤ; otherwise 𝑊 = {0, ..., 𝑛 − 1} enumerates all the equivalence classes. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by Mario Carneiro, 2-May-2016.) (Revised by AV, 13-Jun-2019.) |
| ⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝐹 = ((ℤRHom‘𝑌) ↾ 𝑊) & ⊢ 𝑊 = if(𝑁 = 0, ℤ, (0..^𝑁)) ⇒ ⊢ (𝑁 ∈ ℕ0 → 𝐹:𝑊–1-1-onto→𝐵) | ||
| Theorem | zzngim 21571 | The ℤ ring homomorphism is an isomorphism for 𝑁 = 0. (We only show group isomorphism here, but ring isomorphism follows, since it is a bijective ring homomorphism.) (Contributed by Mario Carneiro, 21-Apr-2016.) (Revised by AV, 13-Jun-2019.) |
| ⊢ 𝑌 = (ℤ/nℤ‘0) & ⊢ 𝐿 = (ℤRHom‘𝑌) ⇒ ⊢ 𝐿 ∈ (ℤring GrpIso 𝑌) | ||
| Theorem | znle2 21572 | The ordering of the ℤ/nℤ structure. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) |
| ⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝐹 = ((ℤRHom‘𝑌) ↾ 𝑊) & ⊢ 𝑊 = if(𝑁 = 0, ℤ, (0..^𝑁)) & ⊢ ≤ = (le‘𝑌) ⇒ ⊢ (𝑁 ∈ ℕ0 → ≤ = ((𝐹 ∘ ≤ ) ∘ ◡𝐹)) | ||
| Theorem | znleval 21573 | The ordering of the ℤ/nℤ structure. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) |
| ⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝐹 = ((ℤRHom‘𝑌) ↾ 𝑊) & ⊢ 𝑊 = if(𝑁 = 0, ℤ, (0..^𝑁)) & ⊢ ≤ = (le‘𝑌) & ⊢ 𝑋 = (Base‘𝑌) ⇒ ⊢ (𝑁 ∈ ℕ0 → (𝐴 ≤ 𝐵 ↔ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ (◡𝐹‘𝐴) ≤ (◡𝐹‘𝐵)))) | ||
| Theorem | znleval2 21574 | The ordering of the ℤ/nℤ structure. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) |
| ⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝐹 = ((ℤRHom‘𝑌) ↾ 𝑊) & ⊢ 𝑊 = if(𝑁 = 0, ℤ, (0..^𝑁)) & ⊢ ≤ = (le‘𝑌) & ⊢ 𝑋 = (Base‘𝑌) ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 ≤ 𝐵 ↔ (◡𝐹‘𝐴) ≤ (◡𝐹‘𝐵))) | ||
| Theorem | zntoslem 21575 | Lemma for zntos 21576. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) |
| ⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝐹 = ((ℤRHom‘𝑌) ↾ 𝑊) & ⊢ 𝑊 = if(𝑁 = 0, ℤ, (0..^𝑁)) & ⊢ ≤ = (le‘𝑌) & ⊢ 𝑋 = (Base‘𝑌) ⇒ ⊢ (𝑁 ∈ ℕ0 → 𝑌 ∈ Toset) | ||
| Theorem | zntos 21576 | The ℤ/nℤ structure is a totally ordered set. (The order is not respected by the operations, except in the case 𝑁 = 0 when it coincides with the ordering on ℤ.) (Contributed by Mario Carneiro, 15-Jun-2015.) |
| ⊢ 𝑌 = (ℤ/nℤ‘𝑁) ⇒ ⊢ (𝑁 ∈ ℕ0 → 𝑌 ∈ Toset) | ||
| Theorem | znhash 21577 | The ℤ/nℤ structure has 𝑛 elements. (Contributed by Mario Carneiro, 15-Jun-2015.) |
| ⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝐵 = (Base‘𝑌) ⇒ ⊢ (𝑁 ∈ ℕ → (♯‘𝐵) = 𝑁) | ||
| Theorem | znfi 21578 | The ℤ/nℤ structure is a finite ring. (Contributed by Mario Carneiro, 2-May-2016.) |
| ⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝐵 = (Base‘𝑌) ⇒ ⊢ (𝑁 ∈ ℕ → 𝐵 ∈ Fin) | ||
| Theorem | znfld 21579 | The ℤ/nℤ structure is a finite field when 𝑛 is prime. (Contributed by Mario Carneiro, 15-Jun-2015.) |
| ⊢ 𝑌 = (ℤ/nℤ‘𝑁) ⇒ ⊢ (𝑁 ∈ ℙ → 𝑌 ∈ Field) | ||
| Theorem | znidomb 21580 | The ℤ/nℤ structure is a domain (and hence a field) precisely when 𝑛 is prime. (Contributed by Mario Carneiro, 15-Jun-2015.) |
| ⊢ 𝑌 = (ℤ/nℤ‘𝑁) ⇒ ⊢ (𝑁 ∈ ℕ → (𝑌 ∈ IDomn ↔ 𝑁 ∈ ℙ)) | ||
| Theorem | znchr 21581 | Cyclic rings are defined by their characteristic. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
| ⊢ 𝑌 = (ℤ/nℤ‘𝑁) ⇒ ⊢ (𝑁 ∈ ℕ0 → (chr‘𝑌) = 𝑁) | ||
| Theorem | znunit 21582 | The units of ℤ/nℤ are the integers coprime to the base. (Contributed by Mario Carneiro, 18-Apr-2016.) |
| ⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝑈 = (Unit‘𝑌) & ⊢ 𝐿 = (ℤRHom‘𝑌) ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) → ((𝐿‘𝐴) ∈ 𝑈 ↔ (𝐴 gcd 𝑁) = 1)) | ||
| Theorem | znunithash 21583 | The size of the unit group of ℤ/nℤ. (Contributed by Mario Carneiro, 19-Apr-2016.) |
| ⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝑈 = (Unit‘𝑌) ⇒ ⊢ (𝑁 ∈ ℕ → (♯‘𝑈) = (ϕ‘𝑁)) | ||
| Theorem | znrrg 21584 | The regular elements of ℤ/nℤ are exactly the units. (This theorem fails for 𝑁 = 0, where all nonzero integers are regular, but only ±1 are units.) (Contributed by Mario Carneiro, 18-Apr-2016.) |
| ⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝑈 = (Unit‘𝑌) & ⊢ 𝐸 = (RLReg‘𝑌) ⇒ ⊢ (𝑁 ∈ ℕ → 𝐸 = 𝑈) | ||
| Theorem | cygznlem1 21585* | Lemma for cygzn 21589. (Contributed by Mario Carneiro, 21-Apr-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑁 = if(𝐵 ∈ Fin, (♯‘𝐵), 0) & ⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ · = (.g‘𝐺) & ⊢ 𝐿 = (ℤRHom‘𝑌) & ⊢ 𝐸 = {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = 𝐵} & ⊢ (𝜑 → 𝐺 ∈ CycGrp) & ⊢ (𝜑 → 𝑋 ∈ 𝐸) ⇒ ⊢ ((𝜑 ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → ((𝐿‘𝐾) = (𝐿‘𝑀) ↔ (𝐾 · 𝑋) = (𝑀 · 𝑋))) | ||
| Theorem | cygznlem2a 21586* | Lemma for cygzn 21589. (Contributed by Mario Carneiro, 23-Dec-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑁 = if(𝐵 ∈ Fin, (♯‘𝐵), 0) & ⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ · = (.g‘𝐺) & ⊢ 𝐿 = (ℤRHom‘𝑌) & ⊢ 𝐸 = {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = 𝐵} & ⊢ (𝜑 → 𝐺 ∈ CycGrp) & ⊢ (𝜑 → 𝑋 ∈ 𝐸) & ⊢ 𝐹 = ran (𝑚 ∈ ℤ ↦ 〈(𝐿‘𝑚), (𝑚 · 𝑋)〉) ⇒ ⊢ (𝜑 → 𝐹:(Base‘𝑌)⟶𝐵) | ||
| Theorem | cygznlem2 21587* | Lemma for cygzn 21589. (Contributed by Mario Carneiro, 21-Apr-2016.) (Revised by Mario Carneiro, 23-Dec-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑁 = if(𝐵 ∈ Fin, (♯‘𝐵), 0) & ⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ · = (.g‘𝐺) & ⊢ 𝐿 = (ℤRHom‘𝑌) & ⊢ 𝐸 = {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = 𝐵} & ⊢ (𝜑 → 𝐺 ∈ CycGrp) & ⊢ (𝜑 → 𝑋 ∈ 𝐸) & ⊢ 𝐹 = ran (𝑚 ∈ ℤ ↦ 〈(𝐿‘𝑚), (𝑚 · 𝑋)〉) ⇒ ⊢ ((𝜑 ∧ 𝑀 ∈ ℤ) → (𝐹‘(𝐿‘𝑀)) = (𝑀 · 𝑋)) | ||
| Theorem | cygznlem3 21588* | A cyclic group with 𝑛 elements is isomorphic to ℤ / 𝑛ℤ. (Contributed by Mario Carneiro, 21-Apr-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑁 = if(𝐵 ∈ Fin, (♯‘𝐵), 0) & ⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ · = (.g‘𝐺) & ⊢ 𝐿 = (ℤRHom‘𝑌) & ⊢ 𝐸 = {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = 𝐵} & ⊢ (𝜑 → 𝐺 ∈ CycGrp) & ⊢ (𝜑 → 𝑋 ∈ 𝐸) & ⊢ 𝐹 = ran (𝑚 ∈ ℤ ↦ 〈(𝐿‘𝑚), (𝑚 · 𝑋)〉) ⇒ ⊢ (𝜑 → 𝐺 ≃𝑔 𝑌) | ||
| Theorem | cygzn 21589 | A cyclic group with 𝑛 elements is isomorphic to ℤ / 𝑛ℤ, and an infinite cyclic group is isomorphic to ℤ / 0ℤ ≈ ℤ. (Contributed by Mario Carneiro, 21-Apr-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑁 = if(𝐵 ∈ Fin, (♯‘𝐵), 0) & ⊢ 𝑌 = (ℤ/nℤ‘𝑁) ⇒ ⊢ (𝐺 ∈ CycGrp → 𝐺 ≃𝑔 𝑌) | ||
| Theorem | cygth 21590* | The "fundamental theorem of cyclic groups". Cyclic groups are exactly the additive groups ℤ / 𝑛ℤ, for 0 ≤ 𝑛 (where 𝑛 = 0 is the infinite cyclic group ℤ), up to isomorphism. (Contributed by Mario Carneiro, 21-Apr-2016.) |
| ⊢ (𝐺 ∈ CycGrp ↔ ∃𝑛 ∈ ℕ0 𝐺 ≃𝑔 (ℤ/nℤ‘𝑛)) | ||
| Theorem | cyggic 21591 | Cyclic groups are isomorphic precisely when they have the same order. (Contributed by Mario Carneiro, 21-Apr-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐶 = (Base‘𝐻) ⇒ ⊢ ((𝐺 ∈ CycGrp ∧ 𝐻 ∈ CycGrp) → (𝐺 ≃𝑔 𝐻 ↔ 𝐵 ≈ 𝐶)) | ||
| Theorem | frgpcyg 21592 | A free group is cyclic iff it has zero or one generator. (Contributed by Mario Carneiro, 21-Apr-2016.) (Proof shortened by AV, 18-Apr-2021.) |
| ⊢ 𝐺 = (freeGrp‘𝐼) ⇒ ⊢ (𝐼 ≼ 1o ↔ 𝐺 ∈ CycGrp) | ||
| Theorem | freshmansdream 21593 | For a prime number 𝑃, if 𝑋 and 𝑌 are members of a commutative ring 𝑅 of characteristic 𝑃, then ((𝑋 + 𝑌)↑𝑃) = ((𝑋↑𝑃) + (𝑌↑𝑃)). This theorem is sometimes referred to as "the freshman's dream" . (Contributed by Thierry Arnoux, 18-Sep-2023.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ ↑ = (.g‘(mulGrp‘𝑅)) & ⊢ 𝑃 = (chr‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑃 ↑ (𝑋 + 𝑌)) = ((𝑃 ↑ 𝑋) + (𝑃 ↑ 𝑌))) | ||
| Theorem | frobrhm 21594* | In a commutative ring with prime characteristic, the Frobenius function 𝐹 is a ring endomorphism, thus named the Frobenius endomorphism. (Contributed by Thierry Arnoux, 31-May-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑃 = (chr‘𝑅) & ⊢ ↑ = (.g‘(mulGrp‘𝑅)) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝑃 ↑ 𝑥)) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑃 ∈ ℙ) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑅)) | ||
| Theorem | cnmsgnsubg 21595 | The signs form a multiplicative subgroup of the complex numbers. (Contributed by Stefan O'Rear, 28-Aug-2015.) |
| ⊢ 𝑀 = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0})) ⇒ ⊢ {1, -1} ∈ (SubGrp‘𝑀) | ||
| Theorem | cnmsgnbas 21596 | The base set of the sign subgroup of the complex numbers. (Contributed by Stefan O'Rear, 28-Aug-2015.) |
| ⊢ 𝑈 = ((mulGrp‘ℂfld) ↾s {1, -1}) ⇒ ⊢ {1, -1} = (Base‘𝑈) | ||
| Theorem | cnmsgngrp 21597 | The group of signs under multiplication. (Contributed by Stefan O'Rear, 28-Aug-2015.) |
| ⊢ 𝑈 = ((mulGrp‘ℂfld) ↾s {1, -1}) ⇒ ⊢ 𝑈 ∈ Grp | ||
| Theorem | psgnghm 21598 | The sign is a homomorphism from the finitary permutation group to the numeric signs. (Contributed by Stefan O'Rear, 28-Aug-2015.) |
| ⊢ 𝑆 = (SymGrp‘𝐷) & ⊢ 𝑁 = (pmSgn‘𝐷) & ⊢ 𝐹 = (𝑆 ↾s dom 𝑁) & ⊢ 𝑈 = ((mulGrp‘ℂfld) ↾s {1, -1}) ⇒ ⊢ (𝐷 ∈ 𝑉 → 𝑁 ∈ (𝐹 GrpHom 𝑈)) | ||
| Theorem | psgnghm2 21599 | The sign is a homomorphism from the finite symmetric group to the numeric signs. (Contributed by Stefan O'Rear, 28-Aug-2015.) |
| ⊢ 𝑆 = (SymGrp‘𝐷) & ⊢ 𝑁 = (pmSgn‘𝐷) & ⊢ 𝑈 = ((mulGrp‘ℂfld) ↾s {1, -1}) ⇒ ⊢ (𝐷 ∈ Fin → 𝑁 ∈ (𝑆 GrpHom 𝑈)) | ||
| Theorem | psgninv 21600 | The sign of a permutation equals the sign of the inverse of the permutation. (Contributed by SO, 9-Jul-2018.) |
| ⊢ 𝑆 = (SymGrp‘𝐷) & ⊢ 𝑁 = (pmSgn‘𝐷) & ⊢ 𝑃 = (Base‘𝑆) ⇒ ⊢ ((𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃) → (𝑁‘◡𝐹) = (𝑁‘𝐹)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |