Si x e y son sumas de dos cuadrados, entonces xy también lo es
Demostrar con Lean4 que si \(x\) e \(y\) son sumas de dos cuadrados, entonces \(xy\) también lo es
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 |
import Mathlib.Tactic variable {α : Type _} [CommRing α] variable {x y : α} -- (suma_de_cuadrados x) afirma que x se puede escribir como la suma -- de dos cuadrados. def suma_de_cuadrados (x : α) := ∃ a b, x = a^2 + b^2 example (hx : suma_de_cuadrados x) (hy : suma_de_cuadrados y) : suma_de_cuadrados (x * y) := by sorry |
Read More «Si x e y son sumas de dos cuadrados, entonces xy también lo es»