le_iff_exists_mul' — Mathlib

English

For a canonically ordered commutative magma, a ≤ b is equivalent to ∃ c with b = c·a.

Русский

Для канонически упорядоченной коммутативной магмы выполнено: a ≤ b эквивалентно существованию c such that b = c·a.

LaTeX

$$$a \le b \iff \exists c\, (b = c\,a)$$$

Lean4

@[to_additive]
theorem le_iff_exists_mul' : a ≤ b ↔ ∃ c, b = c * a := by simp only [mul_comm _ a, le_iff_exists_mul]

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