of_comp — Mathlib

English

If the composition f ∘ x is algebraically independent over R in A', then x is algebraically independent over R in A.

Русский

Если композиция f ∘ x алгебраически независима над R в A', то x алгебраически независим над R в A.

LaTeX

$$$\\text{AlgebraicIndependent } R\\, (f \\circ x) \\Rightarrow \\text{AlgebraicIndependent } R\\, x$$$

Lean4

theorem of_comp (f : A →ₐ[R] A') (hfv : AlgebraicIndependent R (f ∘ x)) : AlgebraicIndependent R x :=
  by
  have : aeval (f ∘ x) = f.comp (aeval x) := by ext; simp
  rw [AlgebraicIndependent, this, AlgHom.coe_comp] at hfv
  exact hfv.of_comp

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