adjoin_natCast

Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

URI: https://scilib.ai/kg/mathlib#IntermediateField.adjoin_natCast

English

Similarly, the subfield generated by a natural number inside E over F is the bottom field.

Русский

Аналогично, подполе, порождаемое натуральным числом n внутри E над F, равно ⊥.

LaTeX

$$$F\langle n \rangle = \bot \quad (n \in \mathbb{N})$$$

Lean4

@[simp]
theorem adjoin_natCast (n : ℕ) : F⟮(n : E)⟯ = ⊥ :=
  adjoin_simple_eq_bot_iff.mpr (natCast_mem ⊥ n)

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

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

Разделы

Аффилиация

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