isSquare_sign_iff — Mathlib

English

For any integer z, z.sign is a nonnegative square iff z ≥ 0.

Русский

Для любого целого z знак z является неотрицательным квадратом тогда и только тогда, когда z ≥ 0.

LaTeX

$$$\\operatorname{IsSquare}(z.sign) \\iff 0 \\le z$$$

Lean4

@[simp]
theorem isSquare_sign_iff {z : ℤ} : IsSquare z.sign ↔ 0 ≤ z := by
  induction z using Int.induction_on with
  | zero => simpa using ⟨0, by simp⟩
  | succ => norm_cast; simp
  | pred =>
    rw [sign_eq_neg_one_of_neg (by cutsat), ← neg_add', Int.neg_nonneg]
    norm_cast
    simp only [reduceNeg, le_zero_eq, Nat.add_eq_zero, succ_ne_self, and_false, iff_false]
    rintro ⟨a | a, ⟨⟩⟩

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