instSubtypeMemSubringCenter — Mathlib

English

There exists an algebraic structure on the subtype of elements in the center of a ring, compatible with the ambient ring structure.

Русский

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

LaTeX

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

Lean4

instance {R : Type*} [Ring R] : Algebra (Subring.center R) R
    where
  algebraMap :=
    { toFun := Subtype.val
      map_one' := rfl
      map_mul' _ _ := rfl
      map_zero' := rfl
      map_add' _ _ := rfl }
  commutes' r x := (Subring.mem_center_iff.1 r.2 x).symm
  smul_def' _ _ := rfl

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