Unicidad de inversos en monoides conmutativos
Demostrar que en los monoides conmutativos, si un elemento tiene un inverso por la derecha, dicho inverso es único.
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 10 |
import algebra.group.basic variables {M : Type} [comm_monoid M] variables {x y z : M} example (hy : x * y = 1) (hz : x * z = 1) : y = z := sorry |
[expand title=»Soluciones con Lean»]
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 |
import algebra.group.basic variables {M : Type} [comm_monoid M] variables {x y z : M} -- 1ª demostración -- =============== example (hy : x * y = 1) (hz : x * z = 1) : y = z := calc y = 1 * y : (one_mul y).symm ... = (x * z) * y : congr_arg (* y) hz.symm ... = (z * x) * y : congr_arg (* y) (mul_comm x z) ... = z * (x * y) : mul_assoc z x y ... = z * 1 : congr_arg ((*) z) hy ... = z : mul_one z -- 2ª demostración -- =============== example (hy : x * y = 1) (hz : x * z = 1) : y = z := calc y = 1 * y : by simp only [one_mul] ... = (x * z) * y : by simp only [hz] ... = (z * x) * y : by simp only [mul_comm] ... = z * (x * y) : by simp only [mul_assoc] ... = z * 1 : by simp only [hy] ... = z : by simp only [mul_one] -- 3ª demostración -- =============== example (hy : x * y = 1) (hz : x * z = 1) : y = z := calc y = 1 * y : by simp ... = (x * z) * y : by simp [hz] ... = (z * x) * y : by simp [mul_comm] ... = z * (x * y) : by simp [mul_assoc] ... = z * 1 : by simp [hy] ... = z : by simp -- 4ª demostración -- =============== example (hy : x * y = 1) (hz : x * z = 1) : y = z := begin apply left_inv_eq_right_inv _ hz, rw mul_comm, exact hy, end -- 5ª demostración -- =============== example (hy : x * y = 1) (hz : x * z = 1) : y = z := left_inv_eq_right_inv (trans (mul_comm _ _) hy) hz -- 6ª demostración -- =============== example (hy : x * y = 1) (hz : x * z = 1) : y = z := inv_unique hy hz |
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="isar"> y otra con </pre>
[/expand]
[expand title=»Soluciones con Isabelle/HOL»]
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 |
theory Unicidad_de_inversos_en_monoides imports Main begin context comm_monoid begin (* 1ª demostración *) lemma assumes "x * y = 1" "x * z = 1" shows "y = z" proof - have "y = 1 * y" by (simp only: left_neutral) also have "… = (x * z) * y" by (simp only: ‹x * z = 1›) also have "… = (z * x) * y" by (simp only: commute) also have "… = z * (x * y)" by (simp only: assoc) also have "… = z * 1" by (simp only: ‹x * y = 1›) also have "… = z" by (simp only: right_neutral) finally show "y = z" by this qed (* 2ª demostración *) lemma assumes "x * y = 1" "x * z = 1" shows "y = z" proof - have "y = 1 * y" by simp also have "… = (x * z) * y" using assms(2) by simp also have "… = (z * x) * y" by simp also have "… = z * (x * y)" by simp also have "… = z * 1" using assms(1) by simp also have "… = z" by simp finally show "y = z" by this qed (* 3ª demostración *) lemma assumes "x * y = 1" "x * z = 1" shows "y = z" using assms by auto end end |
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]