Theorems · Theorem · commutative algebra

AddSubgroup.relIndex_eq_natAbs_det

∀ {E : Type u_1} [inst : AddCommGroup E] (L₁ L₂ : AddSubgroup E) (H : L₁ ≤ L₂) {ι : Type u_2} [inst_1 : DecidableEq ι]
  [inst_2 : Fintype ι] (b₁ : Module.Basis ι ℤ ↥(AddSubgroup.toIntSubmodule L₁))
  (b₂ : Module.Basis ι ℤ ↥(AddSubgroup.toIntSubmodule L₂)), L₁.relIndex L₂ = (b₂.det fun i => ⟨↑(b₁ i), ⋯⟩).natAbs

Defined in

Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient

Cited by

2 results in Mathlib

Foundations

Depth 135 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommGroupDecidableEqFintype