La semana en Calculemus (16 de septiembre de 2023)
Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades:
- 1. En ℝ, |a| – |b| ≤ |a – b|
- 2. Si x, y, z ∈ ℕ, entonces x divide a yxz
- 3. Si x divide a w, entonces también divide a y(xz)+x²+w²
- 4. Conmutatividad del máximo común divisor
- 5. En los retículos, x ⊓ y = y ⊓ x
A continuación se muestran las soluciones.
Read More “La semana en Calculemus (16 de septiembre de 2023)”