instCoeTCOrderMonoidWithZeroHomOfOrderHomClassOfMonoidWithZeroHomClass

Mathlib.Algebra.Order.Hom.MonoidWithZero

URI: https://scilib.ai/kg/mathlib#instCoeTCOrderMonoidWithZeroHomOfOrderHomClassOfMonoidWithZeroHomClass

English

For any e, y = e.symm x iff e y = x.

Русский

Для любого e: y = e.symm x тогда и только тогда, когда e y = x.

LaTeX

$$$y = e^{-1}(x) \\iff e(y) = x$$$

Lean4

instance [OrderHomClass F α β] [MonoidWithZeroHomClass F α β] : CoeTC F (α →*₀o β) :=
  ⟨OrderMonoidWithZeroHomClass.toOrderMonoidWithZeroHom⟩

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

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

Разделы

Аффилиация

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