coprime_card_of_isCyclic_prod — Mathlib

English

If M and N are finite groups and M × N is cyclic, then the orders of M and N are coprime.

Русский

Если M и N конечные группы и M × N циклична, то порядки M и N взаимно просты.

LaTeX

$$$IsCyclic(M \times N) \Rightarrow \gcd(|M|, |N|) = 1$$$

Lean4

@[to_additive coprime_card_of_isAddCyclic_prod]
theorem coprime_card_of_isCyclic_prod [Finite M] [Finite N] : (Nat.card M).Coprime (Nat.card N) :=
  by
  have hM := isCyclic_left_of_prod M N
  have hN := isCyclic_right_of_prod M N
  let _ := cyc.commGroup; let _ := hM.commGroup; let _ := hN.commGroup
  rw [IsCyclic.iff_exponent_eq_card, Monoid.exponent_prod, Nat.card_prod, lcm_eq_nat_lcm] at *
  simpa only [hM, hN, Nat.lcm_eq_mul_iff, Nat.card_pos.ne', false_or] using cyc

Похожие утверждения