discr_eq_discr — Mathlib

English

If f is a ℚ-algebra isomorphism between K and L, then the discriminants agree: discr K = discr L.

Русский

Если f — изоморфизм ℚ-алгебр между K и L, то дискриминанты совпадают: discr K = discr L.

LaTeX

$$$$\\operatorname{discr} K = \\operatorname{discr} L$$$$

Lean4

theorem discr_eq_discr {ι : Type*} [Fintype ι] [DecidableEq ι] (b : Basis ι ℤ (𝓞 K)) : Algebra.discr ℤ b = discr K :=
  by
  let b₀ := Basis.reindex (RingOfIntegers.basis K) (Basis.indexEquiv (RingOfIntegers.basis K) b)
  rw [Algebra.discr_eq_discr (𝓞 K) b b₀, Basis.coe_reindex, Algebra.discr_reindex]

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