Lean4

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

• 1. Si bc = ef, entonces ((ab)c)d = ((ae)f)d
• 2. Si c = ba-d y d = ab, entonces c = 0
• 3. (a+b)(a+b) = aa+2ab+bb
• 4. (a+b)(c+d) = ac+ad+bc+bd
• 5. (a+b)(a-b) = a²-b²

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