Inverso del producto
Sea G un grupo y a, b ∈ G. Entonces,
1 |
(a * b)⁻¹ = b⁻¹ * a⁻¹ |
Para ello, completar la siguiente teoría de Lean:
1 2 3 4 5 6 7 8 9 |
import algebra.group.basic universe u variables {G : Type u} [group G] variables {a b : G} example : (a * b)⁻¹ = b⁻¹ * a⁻¹ := begin 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 |
import algebra.group.basic universe u variables {G : Type u} [group G] variables {a b : G} -- 1ª demostración -- =============== example : (a * b)⁻¹ = b⁻¹ * a⁻¹ := begin apply inv_eq_of_mul_eq_one, calc a * b * (b⁻¹ * a⁻¹) = ((a * b) * b⁻¹) * a⁻¹ : (mul_assoc _ _ _).symm ... = (a * (b * b⁻¹)) * a⁻¹ : congr_arg (* a⁻¹) (mul_assoc a _ _) ... = (a * 1) * a⁻¹ : congr_arg2 _ (congr_arg _ (mul_inv_self b)) rfl ... = a * a⁻¹ : congr_arg (* a⁻¹) (mul_one a) ... = 1 : mul_inv_self a end -- 2ª demostración -- =============== example : (a * b)⁻¹ = b⁻¹ * a⁻¹ := begin apply inv_eq_of_mul_eq_one, calc a * b * (b⁻¹ * a⁻¹) = ((a * b) * b⁻¹) * a⁻¹ : by simp only [mul_assoc] ... = (a * (b * b⁻¹)) * a⁻¹ : by simp only [mul_assoc] ... = (a * 1) * a⁻¹ : by simp only [mul_inv_self] ... = a * a⁻¹ : by simp only [mul_one] ... = 1 : by simp only [mul_inv_self] end -- 3ª demostración -- =============== example : (a * b)⁻¹ = b⁻¹ * a⁻¹ := begin apply inv_eq_of_mul_eq_one, calc a * b * (b⁻¹ * a⁻¹) = ((a * b) * b⁻¹) * a⁻¹ : by simp [mul_assoc] ... = (a * (b * b⁻¹)) * a⁻¹ : by simp ... = (a * 1) * a⁻¹ : by simp ... = a * a⁻¹ : by simp ... = 1 : by simp, end -- 4ª demostración -- =============== example : (a * b)⁻¹ = b⁻¹ * a⁻¹ := mul_inv_rev a b -- 5ª demostración -- =============== example : (a * b)⁻¹ = b⁻¹ * a⁻¹ := by simp |
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»]
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 |
theory Inverso_del_producto imports Main begin context group begin (* 1ª demostración *) lemma "inverse (a * b) = inverse b * inverse a" proof (rule inverse_unique) have "(a * b) * (inverse b * inverse a) = ((a * b) * inverse b) * inverse a" by (simp only: assoc) also have "… = (a * (b * inverse b)) * inverse a" by (simp only: assoc) also have "… = (a * 1) * inverse a" by (simp only: right_inverse) also have "… = a * inverse a" by (simp only: right_neutral) also have "… = 1" by (simp only: right_inverse) finally show "a * b * (inverse b * inverse a) = 1" by this qed (* 2ª demostración *) lemma "inverse (a * b) = inverse b * inverse a" proof (rule inverse_unique) have "(a * b) * (inverse b * inverse a) = ((a * b) * inverse b) * inverse a" by (simp only: assoc) also have "… = (a * (b * inverse b)) * inverse a" by (simp only: assoc) also have "… = (a * 1) * inverse a" by simp also have "… = a * inverse a" by simp also have "… = 1" by simp finally show "a * b * (inverse b * inverse a) = 1" . qed (* 3ª demostración *) lemma "inverse (a * b) = inverse b * inverse a" proof (rule inverse_unique) have "a * b * (inverse b * inverse a) = a * (b * inverse b) * inverse a" by (simp only: assoc) also have "… = 1" by simp finally show "a * b * (inverse b * inverse a) = 1" . qed (* 4ª demostración *) lemma "inverse (a * b) = inverse b * inverse a" by (simp only: inverse_distrib_swap) (* ?ª demostración *) 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]
Referencia
Propiedad 3.19 del libro Abstract algebra: Theory and applications de Thomas W. Judson.