singleton_one_of_bot_eq_top — Mathlib

English

If the bottom subalgebra equals the top, then the cyclotomic extension for {1} over A → B holds.

Русский

Если нижняя подалгебра равна верхней, то IsCyclotomicExtension {1} A B выполняется.

LaTeX

$$$(\\bot : Subalgebra\\, A B) = \\top \\quad\\Rightarrow\\quad IsCyclotomicExtension\\{1\\} A B$$$

Lean4

/-- If `(⊥ : SubAlgebra A B) = ⊤`, then `IsCyclotomicExtension {1} A B`. -/
theorem singleton_one_of_bot_eq_top (h : (⊥ : Subalgebra A B) = ⊤) : IsCyclotomicExtension { 1 } A B :=
  by
  convert eq_self_sdiff_zero _ A B ▸ (iff_union_singleton_one _ A _).1 (singleton_zero_of_bot_eq_top h)
  simp

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