adjoin_singleton_eq_range_aeval — Mathlib

English

For any a ∈ algebra, the subalgebra generated by a equals the range of the evaluation map aeval a.

Русский

Для любого a в алгебре подалгебра, порождаемая a, равна образу отображения évaluations aeval a.

LaTeX

$$$\\operatorname{adjoin}_R\\{a\\} = (\\mathrm{aeval}\\ a)\\text{.range}$$$

Lean4

theorem _root_.Algebra.adjoin_singleton_eq_range_aeval (x : A) : adjoin R { x } = (aeval x).range := by
  rw [← Algebra.map_top, ← adjoin_X, AlgHom.map_adjoin, Set.image_singleton, aeval_X]

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