card_units — Mathlib

English

For a finite GroupWithZero α, the number of units is card α minus 1.

Русский

Для конечного кольца с нулём α число единиц равно кардиналу α минус 1.

LaTeX

$$$$|\\alpha^{\\times}| = |\\alpha| - 1.$$$$

Lean4

theorem card_units [GroupWithZero α] : Nat.card αˣ = Nat.card α - 1 := by
  classical
  rw [Nat.card_congr unitsEquivNeZero, eq_comm, ← Nat.card_congr (Equiv.sumCompl (· = (0 : α)))]
  rcases finite_or_infinite { a : α // a ≠ 0 }
  · rw [Nat.card_sum, Nat.card_unique, add_tsub_cancel_left]
  · rw [Nat.card_eq_zero_of_infinite, Nat.card_eq_zero_of_infinite, zero_tsub]

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