instAlgebraObjForget — Mathlib

English

There is an algebra structure on the forgetful object of any R-algebra S, inherited from S.carrier.

Русский

Для любого R-алгебраического объекта S существует структура алгебры на забывающем объекте, унаследованная от S.carrier.

LaTeX

$$$\\text{Algebra}_R((\\forget(\\mathrm{AlgCat}\\ R)).\\mathrm{obj} S)$$$

Lean4

instance {S : AlgCat.{v} R} : Algebra R ((forget (AlgCat R)).obj S) :=
  (inferInstance : Algebra R S.carrier)

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