exists_one_lt_mul_of_lt

Mathlib.Algebra.Order.Monoid.Canonical.Defs

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

← MathLib Explorer

English

From a < b one can express b as a times some c with c > 1.

Русский

Из a < b следует представить b как a · c с c > 1.

LaTeX

$$$ a < b \\rightarrow \\exists c > 1,\\; a \\cdot c = b $$$

Lean4

@[to_additive]
theorem exists_one_lt_mul_of_lt (h : a < b) : ∃ (c : _) (_ : 1 < c), a * c = b :=
  by
  obtain ⟨c, hc⟩ := le_iff_exists_mul.1 h.le
  refine ⟨c, one_lt_iff_ne_one.2 ?_, hc.symm⟩
  rintro rfl
  simp [hc] at h

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

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

Разделы

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

Аффилиация

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