isAlgebraic_bot_iff — Mathlib

English

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

Русский

Алгебраичность для нижнего подалгебра слева эквивалентна алгебраичности над R.

LaTeX

$$$\text{IsAlgebraic}(⊥: Subalgebra R S, x) \iff \text{IsAlgebraic}(R, x)$$$

Lean4

theorem isAlgebraic_bot_iff (h : Function.Injective (algebraMap R S)) {x : S} :
    IsAlgebraic (⊥ : Subalgebra R S) x ↔ IsAlgebraic R x :=
  isAlgebraic_ringHom_iff_of_comp_eq (Algebra.botEquivOfInjective h).symm (RingHom.id S) Function.injective_id (by rfl)

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