le_sqrt_of_eq_mul — Mathlib

English

If a = b*c, then either b ≤ a.sqrt or c ≤ a.sqrt.

Русский

Если a = b·c, то либо b ≤ a.sqrt, либо c ≤ a.sqrt.

LaTeX

$$$ a = b c \\Rightarrow b \\le a^.sqrt \\\\lor c \\le a^.sqrt$$$

Lean4

theorem le_sqrt_of_eq_mul {a b c : ℕ} (h : a = b * c) : b ≤ a.sqrt ∨ c ≤ a.sqrt :=
  by
  rcases le_total b c with bc | cb
  · exact Or.inl <| le_sqrt.mpr <| h ▸ mul_le_mul_left b bc
  · exact Or.inr <| le_sqrt.mpr <| h ▸ mul_le_mul_right c cb

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