English
Congruence lemma for Fin addCommGroup structure; congruence respects the additive group structure.
Русский
Лемма согласования для структуры Fin с AddCommGroup; конгруэнтность сохраняет структуру группы.
LaTeX
$$$(\\text{congruence properties of } \\mathrm{Fin}.\\mathrm{addCommGroup})$$$
Lean4
instance addCommGroup (n : ℕ) [NeZero n] : AddCommGroup (Fin n)
where
__ := addCommMonoid n
__ := neg n
neg_add_cancel := fun ⟨a, ha⟩ ↦
Fin.ext <|
(Nat.mod_add_mod _ _ _).trans <|
by
rw [Fin.val_zero, Nat.sub_add_cancel, Nat.mod_self]
exact le_of_lt ha
sub := Fin.sub
sub_eq_add_neg := fun ⟨a, ha⟩ ⟨b, hb⟩ ↦ Fin.ext <| by simp [Fin.sub_def, Fin.neg_def, Fin.add_def, Nat.add_comm]
zsmul := zsmulRec
