algebraicIndependent_iff — Mathlib

English

Under an integral extension, AlgebraicIndependent R x is equivalent to AlgebraicIndependent S x, provided FaithfulSMul and NoZeroDivisors assumptions.

Русский

При интегральном расширении равносильно: AlgebraicIndependent R x эквивалентно AlgebraicIndependent S x при указанных условиях.

LaTeX

$$$$ [Algebra.IsIntegral R S] \Rightarrow ( AlgebraicIndependent R x \iff AlgebraicIndependent S x). $$$$

Lean4

protected theorem algebraicIndependent_iff [Algebra.IsIntegral R S] :
    AlgebraicIndependent R x ↔ AlgebraicIndependent S x :=
  ⟨(·.extendScalars_of_isIntegral _), (·.restrictScalars (FaithfulSMul.algebraMap_injective R S))⟩

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