Theorems · Theorem · commutative algebra

Submodule.natAbs_det_basis_change

∀ {M : Type u_1} [inst : AddCommGroup M] [Module.Free ℤ M] [Module.Finite ℤ M] {ι : Type u_2} [inst_3 : Fintype ι]
  [inst_4 : DecidableEq ι] (b : Module.Basis ι ℤ M) (N : Submodule ℤ M) (bN : Module.Basis ι ℤ ↥N),
  (b.det (Subtype.val ∘ ⇑bN)).natAbs = Nat.card (M ⧸ N)

Let b be a basis for M over ℤ and bN a basis for N over ℤ of the same dimension. Then an alternative way to compute the cardinality of M ⧸ N is given by taking the determinant of bN over b.

Defined in

Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddCommGroupModule.FreeModule.FiniteFintypeDecidableEq