La semana en Calculemus (18 de mayo de 2024)
Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades:
- 1. Si G es un grupo y a, b ∈ G tales que ab = 1 entonces a⁻¹ = b
- 2. Si G es un grupo y a, b ∈ G, entonces (ab)⁻¹ = b⁻¹a⁻¹
- 3. Si G un grupo y a ∈ G, entonces (a⁻¹)⁻¹ = a
- 4. Si G es un grupo y a, b, c ∈ G tales que a·b = a·c, entonces b = c
- 5. Si M es un monoide, a ∈ M y m, n ∈ ℕ, entonces a^(m·n) = (a^m)^n
A continuación se muestran las soluciones.
Read More “La semana en Calculemus (18 de mayo de 2024)”