adjoin_eq_range — Mathlib

English

For any set s, adjoin_R s equals the range of aeval Subtype.val.

Русский

Для множества s верно равенство adjoin_R s = range( aeval Subtype.val ).

LaTeX

$$$$ \operatorname{adjoin} _R s = (\mathrm{MvPolynomial}\.\mathrm{aeval}(\operatorname{Subtype}.val)).range $$$$

Lean4

theorem _root_.Algebra.adjoin_eq_range (s : Set S₁) : Algebra.adjoin R s = (MvPolynomial.aeval ((↑) : s → S₁)).range :=
  by rw [← Algebra.adjoin_range_eq_range_aeval, Subtype.range_coe]

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