Si n² es par, entonces n es par
Demostrar con Lean4 que si \(n²\) es par, entonces \(n\) es par.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Tactic open Nat variable (n : ℕ) example (h : 2 ∣ n ^ 2) : 2 ∣ n := by sorry |