subsemiring

Mathlib.Algebra.Algebra.Tower

URI: https://scilib.ai/kg/mathlib#IsScalarTower.subsemiring

English

If U is a subsemiring of S, then the inclusion U ↪ S together with S → A yields a new IsScalarTower U S A.

Русский

Если U — подполумножение S, тогда включение U ↪ S вместе с S → A образуют новую башню IsScalarTower U S A.

LaTeX

$$$ IsScalarTower\ U\ S\ A$$

Lean4

instance (priority := 999) subsemiring (U : Subsemiring S) : IsScalarTower U S A :=
  of_algebraMap_eq fun _x => rfl

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

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

Разделы

Аффилиация

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