Theorems · Theorem · commutative algebra

AddSubgroup.relIndex_eq_abs_det

∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℚ E] (L₁ L₂ : AddSubgroup E),
  L₁ ≤ L₂ →
    ∀ {ι : Type u_2} [inst_2 : DecidableEq ι] [inst_3 : Fintype ι] (b₁ b₂ : Module.Basis ι ℚ E),
      L₁ = AddSubgroup.closure (Set.range ⇑b₁) →
        L₂ = AddSubgroup.closure (Set.range ⇑b₂) → ↑(L₁.relIndex L₂) = |b₂.det ⇑b₁|

Defined in: Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient
Cited by: 1 results in Mathlib
Foundations: Depth 136 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: AddCommGroup Module DecidableEq Fintype

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites33

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Modulestatement and proof · cited by 20,661
CommRingproof · cited by 17,173
AddCommGroupstatement and proof · cited by 12,871
Fintypestatement and proof · cited by 7,736
Algebra.algebraMapproof · cited by 4,706
Set.rangestatement and proof · cited by 4,705
AddGroupproof · cited by 4,410
Matrixproof · cited by 4,303
AddSubgroupstatement and proof · cited by 3,232
absstatement and proof · cited by 1,814
Module.Basisstatement and proof · cited by 1,477

Cited by1

Results whose statement or proof uses this declaration.

NumberField.absNorm_differentIdealproof · cited by 4