natCard_units_lt — Mathlib

English

If M₀ is finite and nontrivial, then the natural card of units is less than the natural card of M₀.

Русский

Если M₀ конечно и не тривиально, то натуральная картина единиц меньше натуральной картины M₀.

LaTeX

$$$\operatorname{Nat.card}(M_0^{\times}) < \operatorname{Nat.card}(M_0)$$$

Lean4

theorem natCard_units_lt [Finite M₀] : Nat.card M₀ˣ < Nat.card M₀ :=
  by
  have : Fintype M₀ := Fintype.ofFinite M₀
  simpa only [Fintype.card_eq_nat_card] using card_units_lt M₀

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