English
For a commutative ring R and any ideal I, the natural index of the additive subgroup I in R, when viewed in the quotient R/I, maps to zero in R/I (i.e., the natural number [R:I] is zero in the quotient).
Русский
Пусть R — коммутативное кольцо и I — идеал. Натуральный индекс подгруппы I в R, рассмотренный в фактор-мизе R/I, отображается нулём в кольцо R/I (то есть число [R:I] равняется нулю в R/I).
LaTeX
$$$\\text{If } I \\le R,\\; [R:I] \\in \\mathbb{N} \\text{ then } ([R:I])\\!\n = 0 \\text{ in } R/I.$$$
Lean4
theorem index_eq_zero {R : Type*} [CommRing R] (I : Ideal R) : (↑I.toAddSubgroup.index : R ⧸ I) = 0 :=
by
rw [AddSubgroup.index, Nat.card_eq]
split_ifs with hq; swap
· simp
letI : Fintype (R ⧸ I) := @Fintype.ofFinite _ hq
exact Nat.cast_card_eq_zero (R ⧸ I)
