discr_ne_zero

Mathlib.NumberTheory.NumberField.Discriminant.Defs

URI: https://scilib.ai/kg/mathlib#NumberField.discr_ne_zero

← MathLib Explorer

English

For a number field K, the discriminant is nonzero: discr K ≠ 0.

Русский

У числа поля K дискриминант не равен нулю: дискриминант K ≠ 0.

LaTeX

$$$$\\operatorname{discr} K \\neq 0.$$$

Lean4

theorem discr_ne_zero : discr K ≠ 0 :=
  by
  rw [← (Int.cast_injective (α := ℚ)).ne_iff, coe_discr]
  exact Algebra.discr_not_zero_of_basis ℚ (integralBasis K)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru