toMulPosReflectLT

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs

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

English

From PosMulReflectLT α, one obtains MulPosReflectLT α.

Русский

Из PosMulReflectLT α следует MulPosReflectLT α.

LaTeX

$$$MulPosReflectLT(\alpha)$$$

Lean4

theorem toMulPosReflectLT [PosMulReflectLT α] : MulPosReflectLT α :=
  posMulReflectLT_iff_mulPosReflectLT.mp ‹_›

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

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

Разделы

Аффилиация

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