cast_card_eq_zero — Mathlib

English

If R is a finite ring (with additive structure), then the natural embedding of the cardinality of R into R is zero; in particular, the ring has finite characteristic.

Русский

Если R — конечное кольцо, тоCard(R) в R равно нулю; следовательно, характеристика кольца конечна.

LaTeX

$$$|R| \cdot 1_R = 0$$$

Lean4

@[simp]
theorem cast_card_eq_zero (R) [AddGroupWithOne R] [Fintype R] : (Fintype.card R : R) = 0 := by
  rw [← nsmul_one, card_nsmul_eq_zero]

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