botEquiv — Mathlib

English

When F is a field and R is a nontrivial F-algebra, the bottom subalgebra of R is canonically isomorphic to F.

Русский

Для поля F и не тривиального F-алгебра R нижняя подалгебра R канонически изоморфна F.

LaTeX

$$$ \\mathrm{botEquiv} (F,R) : (\\bot : \\mathrm{Subalgebra} F R) \\simeq_{F} F $$$

Lean4

/-- The bottom subalgebra is isomorphic to the field. -/
@[simps! symm_apply]
noncomputable def botEquiv (F R : Type*) [Field F] [Semiring R] [Nontrivial R] [Algebra F R] :
    (⊥ : Subalgebra F R) ≃ₐ[F] F :=
  botEquivOfInjective (RingHom.injective _)

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