isAlgebraic_of_isAlgebraic_bot — Mathlib

English

IsAlgebraic for the bottom subalgebra on the left is equivalent to IsAlgebraic over the base ring.

Русский

Алгебраичность нижнего подалгебра слева эквивалентно алгебраичности над базовым кольцом.

LaTeX

$$$IsAlgebraic(⊥ : Subalgebra R S) x \iff IsAlgebraic(R, x)$ for x ∈ S.$$

Lean4

theorem isAlgebraic_of_isAlgebraic_bot {x : S} (halg : IsAlgebraic (⊥ : Subalgebra R S) x) : IsAlgebraic R x :=
  halg.of_ringHom_of_comp_eq (algebraMap R (⊥ : Subalgebra R S)) (RingHom.id S) (by rintro ⟨_, r, rfl⟩; exact ⟨r, rfl⟩)
    Function.injective_id rfl

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