algebraMap_ofSubring_apply — Mathlib

English

There is a natural Algebra instance on the subtype of elements of the center of a ring, giving a canonical R-algebra structure on Subtype fun x => x ∈ Subring.center R.

Русский

Существует естественный экземпляр Algebra на подтипе элементов центра кольца, задающий каноническую R-алгебраическую структуру.

LaTeX

$$instance Algebra (Subtype (mem center)) R$$

Lean4

theorem algebraMap_ofSubring_apply {R : Type*} [CommRing R] (S : Subring R) (x : S) : algebraMap S R x = x :=
  rfl

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