le_maxIdeal

Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

URI: https://scilib.ai/kg/mathlib#AlgebraicClosure.le_maxIdeal

English

For a field k, the span of coefficients spanCoeffs k is contained in the maximal ideal maxIdeal k.

Русский

Пусть k — поле. Замыкание коэффициентов spanCoeffs k содержится в maxIdeal k.

LaTeX

$$$\operatorname{spanCoeffs} k \le \maxIdeal k$$$

Lean4

theorem le_maxIdeal : spanCoeffs k ≤ maxIdeal k :=
  (Classical.choose_spec <| Ideal.exists_le_maximal _ <| spanCoeffs_ne_top k).2

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

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

Разделы

Аффилиация

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