instAlgebra

Mathlib.Algebra.TrivSqZeroExt

URI: https://scilib.ai/kg/mathlib#TrivSqZeroExt.instAlgebra

English

The algebra map from S to tsze R M factors through the left injection.

Русский

Алгебраическое отображение из S в tszeR M факторизуется через inl.

LaTeX

$$$ algebraMap S (tsze R M) = inl \\circ algebraMap S R $$$

Lean4

instance : Algebra R' (tsze R' M) :=
  TrivSqZeroExt.algebra' _ _ _

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

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

Разделы

Аффилиация

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