Autor: José A. Alonso

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)”

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

• 1. Producto de potencias de la misma base en monoides
• 2. Equivalencia de inversos iguales al neutro
• 3. Unicidad de inversos en monoides
• 4. Caracterización de producto igual al primer factor
• 5. Unicidad del elemento neutro en los grupos

A continuación se muestran las soluciones.
Read More “La semana en Calculemus (11 de mayo de 2024)”

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

• 1. Imagen de la interseccion general mediante aplicaciones inyectivas
• 2. Imagen inversa de la unión general
• 3. Imagen inversa de la intersección general
• 4. Teorema de Cantor
• 5. En los monoides, los inversos a la izquierda y a la derecha son iguales

A continuación se muestran las soluciones.
Read More “La semana en Calculemus (4 de mayo de 2024)”

Esta entrada es una recopilación de lecturas compartidas, durante abril de 2024, en Mastodon fundamentalmente sobre programación funcional y demostración asistida por ordenador.

Las lecturas están ordenadas según su fecha de publicación en Mastodon.

Al final de cada artículo se encuentran etiquetas relativas a los sistemas que usa o a su contenido.

Una recopilación de todas las lecturas compartidas se encuentra en GitHub.
Read More “Resumen de lecturas compartidas durante abril de 2024”