instSubsingleton — Mathlib

English

If B is a cyclotomic extension of A by roots of unity of orders S ∪ T, then B is a cyclotomic extension of adjoin A { b ∈ B | ∃ a ∈ S, a ≠ 0, b^a = 1 } with respect to roots of unity of orders in T.

Русский

Если B — циклотомическое расширение A за счёт корней единицы степеней из S ∪ T, то B является циклотомическим расширением над адъин A { b ∈ B | ∃ a ∈ S, a ≠ 0, b^a = 1 } по степеням из T.

LaTeX

$$IsCyclotomicExtension (S ∪ T) A B ⇒ IsCyclotomicExtension T (adjoin A {b ∈ B | ∃ a ∈ S, a ≠ 0 ∧ b^a = 1}) B$$

Lean4

instance instSubsingleton [h : IsCyclotomicExtension ∅ A B] : Subsingleton (Subalgebra A B) :=
  subsingleton_of_bot_eq_top <| by simpa [Algebra.eq_top_iff, isCyclotomicExtension_iff] using h

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