to_subtype_range — Mathlib

English

If x is algebraically independent over R, then the induced family on range x is algebraically independent.

Русский

Если x алгебраически независим над R, то соответствующая последовательность на range x также алгебраически независима.

LaTeX

$$$\\text{AlgIndep}_R(x) \\Rightarrow \\text{AlgIndep}_R(\\mathrm{Subtype}.val|_{\\mathrm{range} x})$$$

Lean4

theorem to_subtype_range (hx : AlgebraicIndependent R x) : AlgebraicIndependent R ((↑) : range x → A) :=
  by
  nontriviality R
  rwa [algebraicIndependent_subtype_range hx.injective]

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