Día: 15 julio 2023

Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades:

• 1. ∀ m n : ℕ, Even n → Even (m * n)
• 2. ∀ a b c ∈ ℝ, (a * b) * c = b * (a * c)
• 3. ∀ a b c ∈ ℝ, (c * b) * a = b * (a * c)
• 4. ∀ a b c ∈ ℝ, a * (b * c) = b * (a * c)
• 5. Si ab = cd y e = f, entonces a(be) = c(df)

A continuación se muestran las soluciones.
Read More “La semana en Calculemus (15 de julio de 2023)”