instAlgebraSubtypeMemSubmoduleOfNat

Mathlib.Algebra.DirectSum.Internal

URI: https://scilib.ai/kg/mathlib#SetLike.GradeZero.instAlgebraSubtypeMemSubmoduleOfNat

English

There is an Algebra structure on A(0) over S inherited from the ambient algebra structure on R.

Русский

Существует структура Algebra над S на A(0), унаследованная от структуры над R.

LaTeX

$$An Algebra S (A_0) exists, induced from Algebra S R.$$

Lean4

instance : Algebra (A 0) R :=
  (SetLike.GradeZero.subalgebra A).toAlgebra

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru