exists_one_le_mul_of_le

Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE

URI: https://scilib.ai/kg/mathlib#exists_one_le_mul_of_le

← MathLib Explorer

English

If a ≤ b, there exists c with 1 ≤ c and a·c = b.

Русский

Если a ≤ b, существует c с 1 ≤ c и a·c = b.

LaTeX

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

Lean4

@[to_additive]
theorem exists_one_le_mul_of_le [MulLeftReflectLE α] (h : a ≤ b) : ∃ c, 1 ≤ c ∧ a * c = b := by
  obtain ⟨c, rfl⟩ := exists_mul_of_le h; exact ⟨c, one_le_of_le_mul_right h, rfl⟩

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

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

Разделы

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

Аффилиация

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