fundSystem_mk — Mathlib

English

The i-th lift of fundSystem corresponds to basisModTorsion via equivalence.

Русский

i-ая лифтирование fundSystem соответствует basisModTorsion через эквивалентность.

LaTeX

$$fundSystem_mk (i : Fin (rank K)) : Additive.ofMul (QuotientGroup.mk (fundSystem K i)) = (basisModTorsion K i)$$

Lean4

theorem fundSystem_mk (i : Fin (rank K)) : Additive.ofMul (QuotientGroup.mk (fundSystem K i)) = (basisModTorsion K i) :=
  by simp_rw [fundSystem, Equiv.apply_eq_iff_eq_symm_apply, Additive.ofMul_symm_eq, Quotient.out_eq']

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