English
Let K be a ring with no zero divisors and G a finite subgroup of the units K^×. Then the cardinality |G|, viewed as an element of K, is nonzero: (|G| : K) ≠ 0.
Русский
Пусть K — кольцо без делителей нуля и G — конечная подгруппа единиц K^×. Тогда отображение количества элементов подгруппы в K не обращается в ноль: (|G| : K) ≠ 0.
LaTeX
$$$\bigl(\text{card } G\bigr : K\bigr) \neq 0$$$
Lean4
theorem card_cast_subgroup_card_ne_zero [Ring K] [NoZeroDivisors K] [Nontrivial K] (G : Subgroup Kˣ) [Fintype G] :
(Fintype.card G : K) ≠ 0 := by
let n := Fintype.card G
intro nzero
have ⟨p, char_p⟩ := CharP.exists K
have hd : p ∣ n := (CharP.cast_eq_zero_iff K p n).mp nzero
cases CharP.char_is_prime_or_zero K p with
| inr pzero => exact (Fintype.card_pos).ne' <| Nat.eq_zero_of_zero_dvd <| pzero ▸ hd
| inl pprime =>
have fact_pprime := Fact.mk pprime
have ⟨x, hx⟩ := exists_prime_orderOf_dvd_card p hd
let u := ((x : Kˣ) : K)
have hu : orderOf u = p := by
rwa [orderOf_units, Subgroup.orderOf_coe]
-- u ^ p = 1 implies (u - 1) ^ p = 0 and hence u = 1 ...
have h : u = 1 := by
rw [← sub_left_inj, sub_self 1]
apply pow_eq_zero (n := p)
rw [sub_pow_char_of_commute, one_pow, ← hu, pow_orderOf_eq_one, sub_self]
exact Commute.one_right u
apply pprime.one_lt.ne
rw [← hu, h, orderOf_one]
