adjoin_intCast

Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

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

English

For any integer n, the subfield generated by n (viewed inside E) over F is the bottom field.

Русский

Для любого целого числа n подполе, порождаемое n в E над F, равно ⊥.

LaTeX

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

Lean4

@[simp]
theorem adjoin_intCast (n : ℤ) : F⟮(n : E)⟯ = ⊥ := by exact adjoin_simple_eq_bot_iff.mpr (intCast_mem ⊥ n)

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

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

Разделы

Аффилиация

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