mem_adjoin_range_iff — Mathlib

English

Characterizes membership in adjoin F (Set.range i) by existential polynomials over i.

Русский

Характеризует принадлежность к адъюнкту через существующие полиномы над i.

LaTeX

$$$x \in \operatorname{adjoin}_F (\operatorname{Set.range} i) \\iff \\exists r,s : MvPolynomial ι F, x = MvPolynomial.aeval i r / MvPolynomial.aeval i s$$$

Lean4

theorem mem_adjoin_range_iff {ι : Type*} (i : ι → E) (x : E) :
    x ∈ adjoin F (Set.range i) ↔ ∃ r s : MvPolynomial ι F, x = MvPolynomial.aeval i r / MvPolynomial.aeval i s := by
  simp_rw [mem_adjoin_iff_div, Algebra.adjoin_range_eq_range_aeval, AlgHom.mem_range, exists_exists_eq_and]

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