José A. AlonsoDemostrar que si a divide a b y a c, entonces también divide a b + c.
Para ello, completar la siguiente teoría de Lean:
import tactic variables {a b c : ℕ} example (divab : a ∣ b) (divac : a ∣ c) : a ∣ (b + c) := sorry |
Demostrar que la relación de divisibilidad es transitiva.
Para ello, completar la siguiente teoría de Lean:
import tactic variables {a b c : ℕ} example (hab : a ∣ b) (hbc : b ∣ c) : a ∣ c := sorry |
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:
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 |