comp — Mathlib

English

If x is algebraically independent, then reindexing by an equivalence e: ι ≃ ι' preserves algebraic independence of f ∘ e and f.

Русский

Если x алгебраически независимо, то перенумеровка индексов по эквиваленту сохраняет алгебраическую независимость функций f и f ∘ e.

LaTeX

$$$\\text{AlgebraicIndependent } R\\, x \\rightarrow\\; \\forall e: ι\\simeq ι',\\; \\text{AlgebraicIndependent } R\\, (f \\circ e) \\leftrightarrow \\text{AlgebraicIndependent } R\\, f$$$

Lean4

theorem comp (f : ι' → ι) (hf : Function.Injective f) : AlgebraicIndependent R (x ∘ f) :=
  by
  intro p q
  simpa [aeval_rename, (rename_injective f hf).eq_iff] using @hx (rename f p) (rename f q)

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