existsMulOfLE

Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE

URI: https://scilib.ai/kg/mathlib#Group.existsMulOfLE

← MathLib Explorer

English

In any group with LE, if a ≤ b, there exists c with a·c = b.

Русский

В группе с LE, если a ≤ b, существует c такого что a·c = b.

LaTeX

$$$\forall a,b \in G, a \le b \Rightarrow \exists c\ (a\cdot c = b).$$$

Lean4

@[to_additive]
instance (priority := 100) existsMulOfLE (α : Type u) [Group α] [LE α] : ExistsMulOfLE α :=
  ⟨fun {a b} _ => ⟨a⁻¹ * b, (mul_inv_cancel_left _ _).symm⟩⟩

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

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

Разделы

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

Аффилиация

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