Un número es par si y solo si lo es su cuadrado
Demostrar con Lean4 que un número es par si y solo si lo es su cuadrado.
Para ello, completar la siguiente teoría de Lean4:
1 2 3 4 5 6 7 8 9 |
import Mathlib.Data.Int.Parity import Mathlib.Tactic open Int variable (n : ℤ) example : Even (n^2) ↔ Even n := by sorry |