Theorems · Theorem · commutative algebra

Submodule.natAbs_det_equiv

∀ {M : Type u_1} [inst : AddCommGroup M] [Module.Free ℤ M] [Module.Finite ℤ M] (N : Submodule ℤ M) {E : Type u_2}
  [inst_3 : EquivLike E M ↥N] [inst_4 : AddEquivClass E M ↥N] (e : E),
  (LinearMap.det (N.subtype ∘ₗ (↑e).toIntLinearMap)).natAbs = Nat.card (M ⧸ N)

Let e : M ≃ N be an additive isomorphism (therefore a ℤ-linear equiv). Then an alternative way to compute the cardinality of the quotient M ⧸ N is given by taking the determinant of e. See natAbs_det_basis_change for a more familiar formulation of this result.

Defined in

Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddCommGroupModule.FreeModule.FiniteEquivLikeAddEquivClass