algebraicIndependent_equiv — Mathlib

English

If e is an equivalence, then AlgebraicIndependent R x is equivalent to AlgebraicIndependent R (f ∘ e).

Русский

Если e — эквивалент, то AlgebraicIndependent R x эквивалентно AlgebraicIndependent R (f ∘ e).

LaTeX

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

Lean4

theorem algebraicIndependent_equiv (e : ι ≃ ι') {f : ι' → A} :
    AlgebraicIndependent R (f ∘ e) ↔ AlgebraicIndependent R f :=
  ⟨fun h => Function.comp_id f ▸ e.self_comp_symm ▸ h.comp _ e.symm.injective, fun h => h.comp _ e.injective⟩

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