instCore

Mathlib.RingTheory.Extension.Presentation.Core

URI: https://scilib.ai/kg/mathlib#Algebra.Presentation.instCore

English

There is an algebra structure of P.Core over R, i.e. P.Core is an R-algebra.

Русский

Существует структура алгебры над R на P.Core, то есть P.Core является R-алгеброй.

LaTeX

$$P.Core is an algebra over R.$$

Lean4

instance : Algebra P.Core R :=
  fast_instance%(inferInstanceAs <| Algebra P.core R)

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

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

Разделы

Аффилиация

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