mul_self_pos — Mathlib

English

For any element a, 0 < a^2 if and only if a ≠ 0.

Русский

Для любого a верно: 0 < a^2 тогда и только тогда a ≠ 0.

LaTeX

$$$0 < a^{2} \\iff a \\neq 0$$$

Lean4

@[simp]
theorem mul_self_pos [ExistsAddOfLE R] [PosMulStrictMono R] [MulPosStrictMono R] [AddLeftStrictMono R]
    [AddLeftReflectLT R] {a : R} : 0 < a * a ↔ a ≠ 0 :=
  by
  constructor
  · rintro h rfl
    rw [mul_zero] at h
    exact h.false
  · intro h
    rcases h.lt_or_gt with h | h
    exacts [mul_pos_of_neg_of_neg h h, mul_pos h h]

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