le_mul_left

Mathlib.Algebra.GroupWithZero.Associated

URI: https://scilib.ai/kg/mathlib#Associates.le_mul_left

English

For any a,b ∈ Associates M, a ≤ b a.

Русский

Для любых a,b ∈ Associates(M): a ≤ b a.

LaTeX

$$$ {a,b : \operatorname{Associates}(M)} \;: \; a \le b a $$$

Lean4

theorem le_mul_left {a b : Associates M} : a ≤ b * a := by rw [mul_comm]; exact le_mul_right

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

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

Разделы

Аффилиация

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