sqLe_smul

Mathlib.NumberTheory.Zsqrtd.Basic

URI: https://scilib.ai/kg/mathlib#Zsqrtd.sqLe_smul

← MathLib Explorer

English

For natural n, if SqLe x c y d, then SqLe (n x) c (n y) d.

Русский

Для натурального n, если SqLe x c y d, то SqLe (n x) c (n y) d.

LaTeX

$$$\forall n \in \mathbb{N}, \ \mathrm{SqLe}(x,c,y,d) \Rightarrow \mathrm{SqLe}(n \cdot x, c, n \cdot y, d)$$$

Lean4

theorem sqLe_smul {c d x y : ℕ} (n : ℕ) (xy : SqLe x c y d) : SqLe (n * x) c (n * y) d := by
  simpa [SqLe, mul_left_comm, mul_assoc] using Nat.mul_le_mul_left (n * n) xy

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

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

Разделы

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

Аффилиация

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