Si x e y son sumas de dos cuadrados, entonces xy también lo es
Demostrar que si x e y son sumas de dos cuadrados, entonces xy también lo es.
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 |
import tactic variables {α : Type*} [comm_ring α] variables {x y : α} -- (es_suma_de_cuadrados x) se verifica si x se puede escribir como la -- suma de dos cuadrados. def es_suma_de_cuadrados (x : α) := ∃ a b, x = a^2 + b^2 example (hx : es_suma_de_cuadrados x) (hy : es_suma_de_cuadrados y) : es_suma_de_cuadrados (x * y) := sorry |
Soluciones con Lean
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 |
import tactic variables {α : Type*} [comm_ring α] variables {x y : α} -- (es_suma_de_cuadrados x) se verifica si x se puede escribir como la -- suma de dos cuadrados. def es_suma_de_cuadrados (x : α) := ∃ a b, x = a^2 + b^2 -- 1ª demostración -- =============== example (hx : es_suma_de_cuadrados x) (hy : es_suma_de_cuadrados y) : es_suma_de_cuadrados (x * y) := begin rcases hx with ⟨a, b, hab : x = a^2 + b^2⟩, rcases hy with ⟨c, d, hcd : y = c^2 + d^2⟩, have h1: x * y = (a*c - b*d)^2 + (a*d + b*c)^2, calc x * y = (a^2 + b^2) * (c^2 + d^2) : by rw [hab, hcd] ... = (a*c - b*d)^2 + (a*d + b*c)^2 : by ring, have h2 : ∃ f, x * y = (a*c - b*d)^2 + f^2, by exact Exists.intro (a*d + b*c) h1, have h3 : ∃ e f, x * y = e^2 + f^2, by exact Exists.intro (a*c - b*d) h2, show es_suma_de_cuadrados (x * y), by exact h3, end -- 2ª demostración -- =============== example (hx : es_suma_de_cuadrados x) (hy : es_suma_de_cuadrados y) : es_suma_de_cuadrados (x * y) := begin rcases hx with ⟨a, b, hab : x = a^2 + b^2⟩, rcases hy with ⟨c, d, hcd : y = c^2 + d^2⟩, have h1: x * y = (a*c - b*d)^2 + (a*d + b*c)^2, calc x * y = (a^2 + b^2) * (c^2 + d^2) : by rw [hab, hcd] ... = (a*c - b*d)^2 + (a*d + b*c)^2 : by ring, have h2 : ∃ e f, x * y = e^2 + f^2, by tauto, show es_suma_de_cuadrados (x * y), by exact h2, end -- 3ª demostración -- =============== example (hx : es_suma_de_cuadrados x) (hy : es_suma_de_cuadrados y) : es_suma_de_cuadrados (x * y) := begin rcases hx with ⟨a, b, hab⟩, rcases hy with ⟨c, d, hcd⟩, rw [hab, hcd], use [a*c - b*d, a*d + b*c], ring, end -- 3ª demostración -- =============== example (hx : es_suma_de_cuadrados x) (hy : es_suma_de_cuadrados y) : es_suma_de_cuadrados (x * y) := begin rcases hx with ⟨a, b, rfl⟩, rcases hy with ⟨c, d, rfl⟩, use [a*c - b*d, a*d + b*c], ring end |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
Referencias
- J. Avigad, K. Buzzard, R.Y. Lewis y P. Massot. Mathematics in Lean, p. 32.
