natAbs_det_basis_change — Mathlib

English

Determinant of the basis-change map between two ℤ-bases gives absNorm I.

Русский

Детерминант отображения смены базиса между двумя базисами ℤ даёт absNorm I.

LaTeX

$$natAbs(det(b ∘ bI)) = absNorm(I)$$

Lean4

/-- Let `b` be a basis for `S` over `ℤ` and `bI` a basis for `I` over `ℤ` of the same dimension.
Then an alternative way to compute the norm of `I` is given by taking the determinant of `bI`
over `b`. -/
theorem natAbs_det_basis_change {ι : Type*} [Fintype ι] [DecidableEq ι] (b : Basis ι ℤ S) (I : Ideal S)
    (bI : Basis ι ℤ I) : (b.det ((↑) ∘ bI)).natAbs = Ideal.absNorm I :=
  Submodule.natAbs_det_basis_change b (I.restrictScalars ℤ) bI

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