toMulPosReflectLE

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs

URI: https://scilib.ai/kg/mathlib#MulRightStrictMono.toMulPosReflectLE

English

From right-strict-monotonicity, deduce a MulPosReflectLE structure.

Русский

Из правой строгой монотонности следует MulPosReflectLE.

LaTeX

$$MulRightStrictMono α ⇒ MulPosReflectLE α$$

Lean4

instance (priority := 100) toMulPosReflectLE [MulRightReflectLE α] : MulPosReflectLE α where
  elim _ _ := ‹MulRightReflectLE α›.elim _

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

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

Разделы

Аффилиация

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