instCovariantClassHSMulLe

Mathlib.Algebra.Algebra.Subalgebra.Pointwise

URI: https://scilib.ai/kg/mathlib#Subalgebra.instCovariantClassHSMulLe

English

There is a CovariantClass instance ensuring mono-compatibility between smul and order.

Русский

Существует экземпляр CovariantClass, обеспечивающий совместимость умножения и порядка.

LaTeX

$$CovariantClass R' (Subalgebra R A) HSMul.hSMul LE.le$$

Lean4

instance : CovariantClass R' (Subalgebra R A) HSMul.hSMul LE.le :=
  ⟨fun _ _ => map_mono⟩

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

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

Разделы

Аффилиация

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