mul_self_inj_of_nonneg

Mathlib.Algebra.Order.Field.Basic

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

← MathLib Explorer

English

If a,b ≥ 0 and a^2 = b^2, then a = b.

Русский

Если a,b ≥ 0 и a^2 = b^2, то a = b.

LaTeX

$$(a0 : 0 \le a) (b0 : 0 \le b) : a * a = b * b \Rightarrow a = b$$

Lean4

theorem mul_self_inj_of_nonneg (a0 : 0 ≤ a) (b0 : 0 ≤ b) : a * a = b * b ↔ a = b :=
  mul_self_eq_mul_self_iff.trans <| or_iff_left_of_imp fun h => by grind

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

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

Разделы

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

Аффилиация

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