instDecidablePredIsSquare — Mathlib

English

There exists a decision procedure for IsSquare on ℤ.

Русский

Существует решение для IsSquare на целых числах.

LaTeX

$$$\exists f:\\mathbb{Z} \to \{0,1\},\forall z:\\mathbb{Z}, f(z)=1 \Leftrightarrow \operatorname{IsSquare}(z)$$$

Lean4

/-- `IsSquare` can be decided on `ℤ` by checking against the square root. -/
instance : DecidablePred (IsSquare : ℤ → Prop) := fun m ↦
  decidable_of_iff' (sqrt m * sqrt m = m) <| by simp_rw [← exists_mul_self m, IsSquare, eq_comm]

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