adjoinRoot_eq_top — Mathlib

English

The subalgebra of AdjoinRoot f generated by the single element root f is the entire algebra, i.e., AdjoinRoot f is generated by root f over R.

Русский

Подалгебра AdjoinRoot f, порождаемая единичным элементом root f, равна всей алгебре; то есть root f порождает всю алгебру над R.

LaTeX

$$$\\operatorname{ Algebra.adjoin }_R\\left(\\{\\mathrm{root}(f)\\}\\right) = \\top$$$

Lean4

theorem adjoinRoot_eq_top : Algebra.adjoin R ({root f} : Set (AdjoinRoot f)) = ⊤ :=
  by
  refine Algebra.eq_top_iff.2 fun x => ?_
  induction x using AdjoinRoot.induction_on with
  | ih p => exact (Algebra.adjoin_singleton_eq_range_aeval R (root f)).symm ▸ ⟨p, aeval_eq p⟩

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