![]() |
Metamath
Proof Explorer Theorem List (p. 216 of 491) | < 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-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dfprm2 21501 | The positive irreducible elements of ℤ are the prime numbers. This is an alternative way to define ℙ. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by AV, 10-Jun-2019.) |
⊢ 𝐼 = (Irred‘ℤring) ⇒ ⊢ ℙ = (ℕ ∩ 𝐼) | ||
Theorem | prmirred 21502 | The irreducible elements of ℤ are exactly the prime numbers (and their negatives). (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by AV, 10-Jun-2019.) |
⊢ 𝐼 = (Irred‘ℤring) ⇒ ⊢ (𝐴 ∈ 𝐼 ↔ (𝐴 ∈ ℤ ∧ (abs‘𝐴) ∈ ℙ)) | ||
Theorem | expghm 21503* | Exponentiation is a group homomorphism from addition to multiplication. (Contributed by Mario Carneiro, 18-Jun-2015.) (Revised by AV, 10-Jun-2019.) |
⊢ 𝑀 = (mulGrp‘ℂfld) & ⊢ 𝑈 = (𝑀 ↾s (ℂ ∖ {0})) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (𝑥 ∈ ℤ ↦ (𝐴↑𝑥)) ∈ (ℤring GrpHom 𝑈)) | ||
Theorem | mulgghm2 21504* | The powers of a group element give a homomorphism from ℤ to a group. The name 1 should not be taken as a constraint as it may be any group element. (Contributed by Mario Carneiro, 13-Jun-2015.) (Revised by AV, 12-Jun-2019.) |
⊢ · = (.g‘𝑅) & ⊢ 𝐹 = (𝑛 ∈ ℤ ↦ (𝑛 · 1 )) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ Grp ∧ 1 ∈ 𝐵) → 𝐹 ∈ (ℤring GrpHom 𝑅)) | ||
Theorem | mulgrhm 21505* | The powers of the element 1 give a ring homomorphism from ℤ to a ring. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 12-Jun-2019.) |
⊢ · = (.g‘𝑅) & ⊢ 𝐹 = (𝑛 ∈ ℤ ↦ (𝑛 · 1 )) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝐹 ∈ (ℤring RingHom 𝑅)) | ||
Theorem | mulgrhm2 21506* | The powers of the element 1 give the unique ring homomorphism from ℤ to a ring. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 12-Jun-2019.) |
⊢ · = (.g‘𝑅) & ⊢ 𝐹 = (𝑛 ∈ ℤ ↦ (𝑛 · 1 )) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (ℤring RingHom 𝑅) = {𝐹}) | ||
Theorem | irinitoringc 21507 | The ring of integers is an initial object in the category of unital rings (within a universe containing the ring of integers). Example 7.2 (6) of [Adamek] p. 101 , and example in [Lang] p. 58. (Contributed by AV, 3-Apr-2020.) |
⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → ℤring ∈ 𝑈) & ⊢ 𝐶 = (RingCat‘𝑈) ⇒ ⊢ (𝜑 → ℤring ∈ (InitO‘𝐶)) | ||
Theorem | nzerooringczr 21508 | There is no zero object in the category of unital rings (at least in a universe which contains the zero ring and the ring of integers). Example 7.9 (3) in [Adamek] p. 103. (Contributed by AV, 18-Apr-2020.) |
⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ 𝐶 = (RingCat‘𝑈) & ⊢ (𝜑 → 𝑍 ∈ (Ring ∖ NzRing)) & ⊢ (𝜑 → 𝑍 ∈ 𝑈) & ⊢ (𝜑 → ℤring ∈ 𝑈) ⇒ ⊢ (𝜑 → (ZeroO‘𝐶) = ∅) | ||
In this subsubsection, an example is given for a condition for a non-unital ring to be unital. This example is already mentioned in the comment for df-subrg 20586: " The subset (ℤ × {0}) of (ℤ × ℤ) (where multiplication is componentwise) contains the false identity 〈1, 0〉 which preserves every element of the subset and thus appears to be the identity of the subset, but is not the identity of the larger ring." The theorems in this subsubsection do not assume that 𝑅 = (ℤring ×s ℤring) is a ring (which can be proven directly very easily, see pzriprng 21525), but provide the prerequisites for ring2idlqusb 21337 to show that 𝑅 is a unital ring, and for ring2idlqus1 21346 to show that 〈1, 1〉 is its ring unity. | ||
Theorem | pzriprnglem1 21509 | Lemma 1 for pzriprng 21525: 𝑅 is a non-unital (actually a unital!) ring. (Contributed by AV, 17-Mar-2025.) |
⊢ 𝑅 = (ℤring ×s ℤring) ⇒ ⊢ 𝑅 ∈ Rng | ||
Theorem | pzriprnglem2 21510 | Lemma 2 for pzriprng 21525: The base set of 𝑅 is the cartesian product of the integers. (Contributed by AV, 17-Mar-2025.) |
⊢ 𝑅 = (ℤring ×s ℤring) ⇒ ⊢ (Base‘𝑅) = (ℤ × ℤ) | ||
Theorem | pzriprnglem3 21511* | Lemma 3 for pzriprng 21525: An element of 𝐼 is an ordered pair. (Contributed by AV, 18-Mar-2025.) |
⊢ 𝑅 = (ℤring ×s ℤring) & ⊢ 𝐼 = (ℤ × {0}) ⇒ ⊢ (𝑋 ∈ 𝐼 ↔ ∃𝑥 ∈ ℤ 𝑋 = 〈𝑥, 0〉) | ||
Theorem | pzriprnglem4 21512 | Lemma 4 for pzriprng 21525: 𝐼 is a subgroup of 𝑅. (Contributed by AV, 18-Mar-2025.) |
⊢ 𝑅 = (ℤring ×s ℤring) & ⊢ 𝐼 = (ℤ × {0}) ⇒ ⊢ 𝐼 ∈ (SubGrp‘𝑅) | ||
Theorem | pzriprnglem5 21513 | Lemma 5 for pzriprng 21525: 𝐼 is a subring of the non-unital ring 𝑅. (Contributed by AV, 18-Mar-2025.) |
⊢ 𝑅 = (ℤring ×s ℤring) & ⊢ 𝐼 = (ℤ × {0}) ⇒ ⊢ 𝐼 ∈ (SubRng‘𝑅) | ||
Theorem | pzriprnglem6 21514 | Lemma 6 for pzriprng 21525: 𝐽 has a ring unity. (Contributed by AV, 19-Mar-2025.) |
⊢ 𝑅 = (ℤring ×s ℤring) & ⊢ 𝐼 = (ℤ × {0}) & ⊢ 𝐽 = (𝑅 ↾s 𝐼) ⇒ ⊢ (𝑋 ∈ 𝐼 → ((〈1, 0〉(.r‘𝐽)𝑋) = 𝑋 ∧ (𝑋(.r‘𝐽)〈1, 0〉) = 𝑋)) | ||
Theorem | pzriprnglem7 21515 | Lemma 7 for pzriprng 21525: 𝐽 is a unital ring. (Contributed by AV, 19-Mar-2025.) |
⊢ 𝑅 = (ℤring ×s ℤring) & ⊢ 𝐼 = (ℤ × {0}) & ⊢ 𝐽 = (𝑅 ↾s 𝐼) ⇒ ⊢ 𝐽 ∈ Ring | ||
Theorem | pzriprnglem8 21516 | Lemma 8 for pzriprng 21525: 𝐼 resp. 𝐽 is a two-sided ideal of the non-unital ring 𝑅. (Contributed by AV, 21-Mar-2025.) |
⊢ 𝑅 = (ℤring ×s ℤring) & ⊢ 𝐼 = (ℤ × {0}) & ⊢ 𝐽 = (𝑅 ↾s 𝐼) ⇒ ⊢ 𝐼 ∈ (2Ideal‘𝑅) | ||
Theorem | pzriprnglem9 21517 | Lemma 9 for pzriprng 21525: The ring unity of the ring 𝐽. (Contributed by AV, 22-Mar-2025.) |
⊢ 𝑅 = (ℤring ×s ℤring) & ⊢ 𝐼 = (ℤ × {0}) & ⊢ 𝐽 = (𝑅 ↾s 𝐼) & ⊢ 1 = (1r‘𝐽) ⇒ ⊢ 1 = 〈1, 0〉 | ||
Theorem | pzriprnglem10 21518 | Lemma 10 for pzriprng 21525: The equivalence classes of 𝑅 modulo 𝐽. (Contributed by AV, 22-Mar-2025.) |
⊢ 𝑅 = (ℤring ×s ℤring) & ⊢ 𝐼 = (ℤ × {0}) & ⊢ 𝐽 = (𝑅 ↾s 𝐼) & ⊢ 1 = (1r‘𝐽) & ⊢ ∼ = (𝑅 ~QG 𝐼) ⇒ ⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → [〈𝑋, 𝑌〉] ∼ = (ℤ × {𝑌})) | ||
Theorem | pzriprnglem11 21519* | Lemma 11 for pzriprng 21525: 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 21520 | Lemma 12 for pzriprng 21525: 𝑄 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 21521 | Lemma 13 for pzriprng 21525: 𝑄 is a unital ring. (Contributed by AV, 23-Mar-2025.) |
⊢ 𝑅 = (ℤring ×s ℤring) & ⊢ 𝐼 = (ℤ × {0}) & ⊢ 𝐽 = (𝑅 ↾s 𝐼) & ⊢ 1 = (1r‘𝐽) & ⊢ ∼ = (𝑅 ~QG 𝐼) & ⊢ 𝑄 = (𝑅 /s ∼ ) ⇒ ⊢ 𝑄 ∈ Ring | ||
Theorem | pzriprnglem14 21522 | Lemma 14 for pzriprng 21525: 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 21523 | 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 21337). (Contributed by AV, 23-Mar-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (ℤring ×s ℤring) ∈ Ring | ||
Theorem | pzriprng1ALT 21524 | 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 21346). (Contributed by AV, 24-Mar-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (1r‘(ℤring ×s ℤring)) = 〈1, 1〉 | ||
Theorem | pzriprng 21525 | The non-unital ring (ℤring ×s ℤring) is unital. Direct proof in contrast to pzriprngALT 21523. (Contributed by AV, 25-Mar-2025.) |
⊢ (ℤring ×s ℤring) ∈ Ring | ||
Theorem | pzriprng1 21526 | The ring unity of the ring (ℤring ×s ℤring). Direct proof in contrast to pzriprng1ALT 21524. (Contributed by AV, 25-Mar-2025.) |
⊢ (1r‘(ℤring ×s ℤring)) = 〈1, 1〉 | ||
Syntax | czrh 21527 | Map the rationals into a field, or the integers into a ring. |
class ℤRHom | ||
Syntax | czlm 21528 | Augment an abelian group with vector space operations to turn it into a ℤ-module. |
class ℤMod | ||
Syntax | cchr 21529 | Syntax for ring characteristic. |
class chr | ||
Syntax | czn 21530 | The ring of integers modulo 𝑛. |
class ℤ/nℤ | ||
Definition | df-zrh 21531 | 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 19098). (Contributed by Mario Carneiro, 13-Jun-2015.) (Revised by AV, 12-Jun-2019.) |
⊢ ℤRHom = (𝑟 ∈ V ↦ ∪ (ℤring RingHom 𝑟)) | ||
Definition | df-zlm 21532 | 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 21533 | 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 21534* | 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 21535 | 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 21536* | Alternate value of the ℤRHom homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ 𝐿 = (ℤRHom‘𝑅) & ⊢ · = (.g‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝐿 = (𝑛 ∈ ℤ ↦ (𝑛 · 1 ))) | ||
Theorem | zrhmulg 21537 | Value of the ℤRHom homomorphism. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ 𝐿 = (ℤRHom‘𝑅) & ⊢ · = (.g‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ ℤ) → (𝐿‘𝑁) = (𝑁 · 1 )) | ||
Theorem | zrhrhmb 21538 | 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 21539 | 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 21540 | Interpretation of 1 in a ring. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
⊢ 𝐿 = (ℤRHom‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝐿‘1) = 1 ) | ||
Theorem | zrh0 21541 | Interpretation of 0 in a ring. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
⊢ 𝐿 = (ℤRHom‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝐿‘0) = 0 ) | ||
Theorem | zrhpropd 21542* | 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 21543 | 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 21544 | Lemma for zlmbas 21546 and zlmplusg 21548. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.) |
⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ 𝐸 = Slot (𝐸‘ndx) & ⊢ (𝐸‘ndx) ≠ (Scalar‘ndx) & ⊢ (𝐸‘ndx) ≠ ( ·𝑠 ‘ndx) ⇒ ⊢ (𝐸‘𝐺) = (𝐸‘𝑊) | ||
Theorem | zlmlemOLD 21545 | Obsolete version of zlmlem 21544 as of 3-Nov-2024. Lemma for zlmbas 21546 and zlmplusg 21548. (Contributed by Mario Carneiro, 2-Oct-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑁 < 5 ⇒ ⊢ (𝐸‘𝐺) = (𝐸‘𝑊) | ||
Theorem | zlmbas 21546 | Base set of a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.) |
⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ 𝐵 = (Base‘𝑊) | ||
Theorem | zlmbasOLD 21547 | Obsolete version of zlmbas 21546 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 21548 | Group operation of a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.) |
⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ + = (+g‘𝑊) | ||
Theorem | zlmplusgOLD 21549 | Obsolete version of zlmbas 21546 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 21550 | 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 21551 | Obsolete version of zlmbas 21546 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 21552 | 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 21553 | Scalar multiplication operation of a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑊 = (ℤMod‘𝐺) & ⊢ · = (.g‘𝐺) ⇒ ⊢ · = ( ·𝑠 ‘𝑊) | ||
Theorem | zlmlmod 21554 | The ℤ-module operation turns an arbitrary abelian group into a left module over ℤ. Also see zlmassa 21940. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑊 = (ℤMod‘𝐺) ⇒ ⊢ (𝐺 ∈ Abel ↔ 𝑊 ∈ LMod) | ||
Theorem | chrval 21555 | Definition substitution of the ring characteristic. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝑂 = (od‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝐶 = (chr‘𝑅) ⇒ ⊢ (𝑂‘ 1 ) = 𝐶 | ||
Theorem | chrcl 21556 | Closure of the characteristic. (Contributed by Mario Carneiro, 23-Sep-2015.) |
⊢ 𝐶 = (chr‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝐶 ∈ ℕ0) | ||
Theorem | chrid 21557 | 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 21558 | 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 21559 | 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 21560 | 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 21561 | A generalization of Fermat's little theorem in a commutative ring 𝐹 of prime characteristic. See fermltl 16817. (Contributed by Thierry Arnoux, 9-Jan-2024.) |
⊢ 𝑃 = (chr‘𝐹) & ⊢ 𝐵 = (Base‘𝐹) & ⊢ ↑ = (.g‘(mulGrp‘𝐹)) & ⊢ 𝐴 = ((ℤRHom‘𝐹)‘𝐸) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝐸 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ CRing) ⇒ ⊢ (𝜑 → (𝑃 ↑ 𝐴) = 𝐴) | ||
Theorem | chrnzr 21562 | Nonzero rings are precisely those with characteristic not 1. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
⊢ (𝑅 ∈ Ring → (𝑅 ∈ NzRing ↔ (chr‘𝑅) ≠ 1)) | ||
Theorem | chrrhm 21563 | The characteristic restriction on ring homomorphisms. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (chr‘𝑆) ∥ (chr‘𝑅)) | ||
Theorem | domnchr 21564 | 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 21565 | 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 21566 | 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 21567 | 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 21568 | 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 21569 | 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 21570 | Lemma for znbas 21579. (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 21571 | Obsolete version of znbaslem 21570 as of 3-Nov-2024. Lemma for znbas 21579. (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 21572 | 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 21573 | Obsolete version of znbas2 21572 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 21574 | 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 21575 | Obsolete version of znadd 21574 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 21576 | 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 21577 | Obsolete version of znadd 21574 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 21578 | 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 21579 | 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 21580 | ℤ/nℤ is a commutative ring. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝑌 = (ℤ/nℤ‘𝑁) ⇒ ⊢ (𝑁 ∈ ℕ0 → 𝑌 ∈ CRing) | ||
Theorem | znzrh2 21581* | 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 21582 | 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 21583 | The ℤ ring homomorphism is a surjection onto ℤ/nℤ. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝐿 = (ℤRHom‘𝑌) ⇒ ⊢ (𝑁 ∈ ℕ0 → 𝐿:ℤ–onto→𝐵) | ||
Theorem | zncyg 21584 | The group ℤ / 𝑛ℤ is cyclic for all 𝑛 (including 𝑛 = 0). (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝑌 = (ℤ/nℤ‘𝑁) ⇒ ⊢ (𝑁 ∈ ℕ0 → 𝑌 ∈ CycGrp) | ||
Theorem | zndvds 21585 | Express equality of equivalence classes in ℤ / 𝑛ℤ in terms of divisibility. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑌) ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐿‘𝐴) = (𝐿‘𝐵) ↔ 𝑁 ∥ (𝐴 − 𝐵))) | ||
Theorem | zndvds0 21586 | Special case of zndvds 21585 when one argument is zero. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝐿 = (ℤRHom‘𝑌) & ⊢ 0 = (0g‘𝑌) ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) → ((𝐿‘𝐴) = 0 ↔ 𝑁 ∥ 𝐴)) | ||
Theorem | znf1o 21587 | 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 21588 | 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 21589 | 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 21590 | 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 21591 | 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 21592 | Lemma for zntos 21593. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) |
⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝐹 = ((ℤRHom‘𝑌) ↾ 𝑊) & ⊢ 𝑊 = if(𝑁 = 0, ℤ, (0..^𝑁)) & ⊢ ≤ = (le‘𝑌) & ⊢ 𝑋 = (Base‘𝑌) ⇒ ⊢ (𝑁 ∈ ℕ0 → 𝑌 ∈ Toset) | ||
Theorem | zntos 21593 | 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 21594 | The ℤ/nℤ structure has 𝑛 elements. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝐵 = (Base‘𝑌) ⇒ ⊢ (𝑁 ∈ ℕ → (♯‘𝐵) = 𝑁) | ||
Theorem | znfi 21595 | The ℤ/nℤ structure is a finite ring. (Contributed by Mario Carneiro, 2-May-2016.) |
⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝐵 = (Base‘𝑌) ⇒ ⊢ (𝑁 ∈ ℕ → 𝐵 ∈ Fin) | ||
Theorem | znfld 21596 | The ℤ/nℤ structure is a finite field when 𝑛 is prime. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝑌 = (ℤ/nℤ‘𝑁) ⇒ ⊢ (𝑁 ∈ ℙ → 𝑌 ∈ Field) | ||
Theorem | znidomb 21597 | 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 21598 | Cyclic rings are defined by their characteristic. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
⊢ 𝑌 = (ℤ/nℤ‘𝑁) ⇒ ⊢ (𝑁 ∈ ℕ0 → (chr‘𝑌) = 𝑁) | ||
Theorem | znunit 21599 | 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 21600 | The size of the unit group of ℤ/nℤ. (Contributed by Mario Carneiro, 19-Apr-2016.) |
⊢ 𝑌 = (ℤ/nℤ‘𝑁) & ⊢ 𝑈 = (Unit‘𝑌) ⇒ ⊢ (𝑁 ∈ ℕ → (♯‘𝑈) = (ϕ‘𝑁)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |