image — Mathlib

English

If hs is algebraic independent, then the image under the inclusion map is also algebraically independent.

Русский

Если hs алгебраически независимо, то образ при включении тоже алгебраически независим.

LaTeX

$$$\text{AlgebraicIndependent}_R \;\text{on } s \Rightarrow \text{AlgebraicIndependent}_R \;\text{on } f''s$$$

Lean4

theorem image {ι} {s : Set ι} {f : ι → A} (hs : AlgebraicIndependent R fun x : s => f x) :
    AlgebraicIndependent R fun x : f '' s => (x : A) := by convert AlgebraicIndependent.image_of_comp s f id hs

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