Step
*
of Lemma
isqrt-of-square
∀[z:ℕ]. (isqrt(z * z) = z ∈ ℤ)
BY
{ Auto }
1
1. z : ℕ
⊢ isqrt(z * z) = z ∈ ℤ
Latex:
Latex:
\mforall{}[z:\mBbbN{}]. (isqrt(z * z) = z)
By
Latex:
Auto
Home
Index