mul_self_inj — Mathlib

English

Let R be a linearly ordered semiring equipped with PosMulStrictMono and MulPosMono. Then for all a, b with a ≥ 0 and b ≥ 0, a^2 = b^2 if and only if a = b.

Русский

Пусть R — линейно упорядоченная полупревращённая (полугольная) структура с неотрицательными элементами, где умножение положительно монотонно. Тогда для любых a, b ≥ 0 верно: a^2 = b^2 тогда и только тогда, когда a = b.

LaTeX

$$$\forall a,b\in R,\ (0\le a)\land (0\le b)\ \Rightarrow\ (a^2 = b^2 \iff a = b)$$$

Lean4

theorem mul_self_inj [PosMulStrictMono R] [MulPosMono R] {a b : R} (h1 : 0 ≤ a) (h2 : 0 ≤ b) : a * a = b * b ↔ a = b :=
  (@strictMonoOn_mul_self R _).eq_iff_eq h1 h2

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