comap_isAlgebraic_iff — Mathlib

English

Another formulation of the equivalence of algebraicity under the fraction field and A.

Русский

Другая формулировка эквивалентности алгебраичности между A и полем дробей A.

LaTeX

$$$\text{Algebra.IsAlgebraic}_A(x) \Leftrightarrow \text{Algebra.IsAlgebraic}_K(x)$$$

Lean4

/-- A ring is algebraic over the ring `A` iff it is algebraic over the field of fractions of `A`.
-/
theorem comap_isAlgebraic_iff [Algebra A C] [Algebra K C] [IsScalarTower A K C] :
    Algebra.IsAlgebraic A C ↔ Algebra.IsAlgebraic K C :=
  ⟨fun h => ⟨fun x => (isAlgebraic_iff A K C).mp (h.isAlgebraic x)⟩, fun h =>
    ⟨fun x => (isAlgebraic_iff A K C).mpr (h.isAlgebraic x)⟩⟩

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