coe_discr — Mathlib

English

The discriminant of K is the same as the discriminant computed from the integral basis, via canonical identifications with ℚ.

Русский

Дискриминант K совпадает с дискриминантом, полученным из интегральной базы через соответствия с ℚ.

LaTeX

$$$$\\operatorname{discr} K = \\operatorname{Algebra.discr}_{\\mathbb{Q}}(\\text{integralBasis }K).$$$$

Lean4

theorem coe_discr : (discr K : ℚ) = Algebra.discr ℚ (integralBasis K) :=
  (Algebra.discr_localizationLocalization ℤ _ K (RingOfIntegers.basis K)).symm

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