card_addChar_le — Mathlib

English

The cardinality of AddChar G R is bounded by |G|; equality may hold in some cases.

Русский

Кардинал AddChar G R ограничен величиной |G|; равенство возможно в некоторых случаях.

LaTeX

$$$|\\operatorname{AddChar}(G,R)| \\le |G|.$$$

Lean4

@[simp]
theorem card_addChar_le [Fintype G] : card (AddChar G R) ≤ card G := by
  simpa only [Module.finrank_fintype_fun_eq_card] using (AddChar.linearIndependent G R).fintype_card_le_finrank

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