toMulPosReflectLT

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs

URI: https://scilib.ai/kg/mathlib#MulPosMono.toMulPosReflectLT

English

PosMulMono α is equivalent to PosMulReflectLT α.

Русский

PosMulMono α эквивалентно PosMulReflectLT α.

LaTeX

$$PosMulMono(\alpha) \iff PosMulReflectLT(\alpha)$$

Lean4

theorem toMulPosReflectLT [MulPosMono α] : MulPosReflectLT α where
  elim := (covariant_le_iff_contravariant_lt _ _ _).1 CovariantClass.elim

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

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

Разделы

Аффилиация

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