Potencias de potencias en monoides

En los monoides se define la potencia con exponentes naturales. En Lean la potencia x^n se caracteriza por los siguientes lemas:

Demostrar que si M es un monoide, a ∈ M y m, n ∈ ℕ, entonces

Indicación: Se puede usar el lema

Para ello, completar la siguiente teoría de Lean:

[expand title=»Soluciones con Lean»]

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Escribe un comentario