adjoin_range_eq_range_aeval — Mathlib

English

The subalgebra adjoined by the range of f equals the range of aeval f.

Русский

Подалгебра, порожденная образами f, равна образу aeval f.

LaTeX

$$$$ \operatorname{adjoin}_R (\operatorname{range} f) = (\mathrm{MvPolynomial}\.\mathrm{aeval} f).\mathrm{range} $$$$

Lean4

theorem _root_.Algebra.adjoin_range_eq_range_aeval : Algebra.adjoin R (Set.range f) = (MvPolynomial.aeval f).range := by
  simp only [← Algebra.map_top, ← MvPolynomial.adjoin_range_X, AlgHom.map_adjoin, ← Set.range_comp, Function.comp_def,
    MvPolynomial.aeval_X]

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