card_units_lt — Mathlib

English

For a finite, nontrivial monoid with zero, the number of units is strictly less than the total number of elements.

Русский

Для конечного ненулевого моноида с нулём число единиц строго меньше общего числа элементов.

LaTeX

$$$|M_0^{\times}| < |M_0|$$$

Lean4

theorem card_units_lt [Fintype M₀] : Fintype.card M₀ˣ < Fintype.card M₀ :=
  Fintype.card_lt_of_injective_of_notMem Units.val Units.val_injective not_isUnit_zero

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