instDecidablePredIsSquare — Mathlib

English

IsSquare on ℚ is decidable by checking whether sqrt(m)·sqrt(m) = m.

Русский

Определимость IsSquare на ℚ достигается проверкой равенства sqrt(m)·sqrt(m) = m.

LaTeX

$$$ \text{IsSquare}(m) \;\iff\; \sqrt{m} \cdot \sqrt{m} = m $$$

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]

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