coe_range — Mathlib

English

If x is algebraically independent, then its range viewed as a subtype injects into A preserving algebraic independence.

Русский

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

LaTeX

$$$\\text{AlgebraicIndependent } R\\, x \\Rightarrow \\text{AlgebraicIndependent } R\\, (\\mathrm{Subtype.val})$$$

Lean4

theorem coe_range : AlgebraicIndependent R ((↑) : range x → A) := by simpa using hx.comp _ (rangeSplitting_injective x)

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