mulLeft₀

Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso

URI: https://scilib.ai/kg/mathlib#OrderIso.mulLeft₀

← MathLib Explorer

English

The left-multiplication isomorphism corresponds to a positive-order isomorphism.

Русский

Левосторонняя умножение образует изоморфизм порядка.

LaTeX

$$OrderIso.mulLeft₀(•, •)$$

Lean4

/-- `Equiv.mulLeft₀` as an order isomorphism. -/
@[simps! +simpRhs]
def mulLeft₀ (a : G₀) (ha : 0 < a) : G₀ ≃o G₀
    where
  toEquiv := .mulLeft₀ a ha.ne'
  map_rel_iff' := mul_le_mul_iff_right₀ ha

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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