algebraicIndependent_equiv' — Mathlib

English

If e is an equivalence and f∘e=g, then AlgebraicIndependent R g ↔ AlgebraicIndependent R f.

Русский

Если e — эквивалент и f∘e=g, тогда AlgebraicIndependent R g ⇔ AlgebraicIndependent R f.

LaTeX

$$$\\text{AlgebraicIndependent } R\\, (f \\circ e) \\iff \\text{AlgebraicIndependent } R\\, f$$$

Lean4

theorem algebraicIndependent_equiv' (e : ι ≃ ι') {f : ι' → A} {g : ι → A} (h : f ∘ e = g) :
    AlgebraicIndependent R g ↔ AlgebraicIndependent R f :=
  h ▸ algebraicIndependent_equiv e

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