index_eq_natAbs_det — Mathlib

English

The index of an additive subgroup L1 in L2 equals the absolute determinant of the corresponding change of basis when L1,L2 have bases of the same rank.

Русский

Индекс подгруппы L1 в L2 равен абсолютному детерминанту соответствующего перехода базисов при равном ранге.

LaTeX

$$$$ L_1.\mathrm{relIndex} L_2 = \big| b_2.det (f) \big| $$$$

Lean4

theorem index_eq_natAbs_det {E : Type*} [AddCommGroup E] {ι : Type*} [DecidableEq ι] [Fintype ι] (bE : Basis ι ℤ E)
    (N : AddSubgroup E) (bN : Basis ι ℤ N) : N.index = (bE.det (bN ·)).natAbs :=
  have : Module.Free ℤ E := Module.Free.of_basis bE
  have : Module.Finite ℤ E := Module.Finite.of_basis bE
  (Submodule.natAbs_det_basis_change bE N.toIntSubmodule bN).symm

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