Theorems · Theorem · group theory
coprime_card_of_isAddCyclic_prod
∀ (M : Type u_4) (N : Type u_5) [inst : AddGroup M] [inst_1 : AddGroup N] [cyc : IsAddCyclic (M × N)] [Finite M] [Finite N], (Nat.card M).Coprime (Nat.card N)
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 103 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites16
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddCommGroupproof · cited by 12,871
- AddGroupstatement and proof · cited by 4,410
- Finitestatement and proof · cited by 3,029
- LT.lt.ne'proof · cited by 1,417
- Nat.cardstatement and proof · cited by 844
- GCDMonoid.lcmproof · cited by 78
- AddMonoid.exponentproof · cited by 70
- IsAddCyclicstatement and proof · cited by 55
- Nat.card_posproof · cited by 36
- Nat.card_prodproof · cited by 24
- lcm_eq_nat_lcmproof · cited by 3
- IsAddCyclic.addCommGroupproof · cited by 2
Cited by2
Results whose statement or proof uses this declaration.
- not_isAddCyclic_prod_of_infinite_nontrivialproof · cited by 2
- AddGroup.isAddCyclic_prod_iffproof · cited by 0