algebraicIndependent_subtype — Mathlib

English

The algebraic independence of the inclusion map s ↪ A is equivalent to the same polynomial-relations condition on A with respect to s.

Русский

Независимость включения s в A эквивалентна такому же условию на A относительно s.

LaTeX

$$$\AlgebraicIndependent R ((\uparrow) : s \to A) \iff \forall p : \mathrm{MvPolynomial} A R,\ p \in \mathrm{supported} R s \to aeval id p = 0 \Rightarrow p = 0$$$

Lean4

theorem algebraicIndependent_subtype {s : Set A} :
    AlgebraicIndependent R ((↑) : s → A) ↔
      ∀ p : MvPolynomial A R, p ∈ MvPolynomial.supported R s → aeval id p = 0 → p = 0 :=
  by apply @algebraicIndependent_comp_subtype _ _ _ id

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