singleton_one_of_algebraMap_bijective

English

If the A-algebra map from A to B is surjective, then IsCyclotomicExtension {1} A B holds.

Русский

Если отображение алгебр A→B сюръективно, то IsCyclotomicExtension {1} A B выполняется.

LaTeX

$$$\\text{Surjective}(\\text{algebraMap } A B) \\Rightarrow IsCyclotomicExtension\\{1\\} A B$$$

Lean4

/-- If `Function.Surjective (algebraMap A B)`, then `IsCyclotomicExtension {1} A B`. -/
theorem singleton_one_of_algebraMap_bijective (h : Function.Surjective (algebraMap A B)) :
    IsCyclotomicExtension { 1 } A B :=
  singleton_one_of_bot_eq_top (surjective_algebraMap_iff.1 h).symm

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