asq_pos

Mathlib.NumberTheory.PellMatiyasevic

URI: https://scilib.ai/kg/mathlib#Pell.asq_pos

English

If a > 1, then a^2 > 0.

Русский

Если a > 1, то a^2 > 0.

LaTeX

$$$ 0 < a^2 $$$

Lean4

theorem asq_pos : 0 < a * a :=
  le_trans (le_of_lt a1) (by have := @Nat.mul_le_mul_left 1 a a (le_of_lt a1); rwa [mul_one] at this)

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

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

Разделы

Аффилиация

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