-
Notifications
You must be signed in to change notification settings - Fork 0
/
Inverso_del_inverso_en_grupos.lean
84 lines (64 loc) · 2.17 KB
/
Inverso_del_inverso_en_grupos.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
78
79
80
81
82
83
84
-- Inverso_del_inverso_en_grupos.lean
-- Inverso del inverso en grupos
-- José A. Alonso Jiménez
-- Sevilla, 7 de julio de 2021
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Sea G un grupo y a ∈ G. Demostrar que
-- (a⁻¹)⁻¹ = a
-- ---------------------------------------------------------------------
import algebra.group.basic
universe u
variables {G : Type u} [group G]
variables {a b : G}
-- 1ª demostración
-- ===============
example : (a⁻¹)⁻¹ = a :=
calc (a⁻¹)⁻¹
= (a⁻¹)⁻¹ * 1 : (mul_one (a⁻¹)⁻¹).symm
... = (a⁻¹)⁻¹ * (a⁻¹ * a) : congr_arg ((*) (a⁻¹)⁻¹) (inv_mul_self a).symm
... = ((a⁻¹)⁻¹ * a⁻¹) * a : (mul_assoc _ _ _).symm
... = 1 * a : congr_arg (* a) (inv_mul_self a⁻¹)
... = a : one_mul a
-- 2ª demostración
-- ===============
example : (a⁻¹)⁻¹ = a :=
calc (a⁻¹)⁻¹
= (a⁻¹)⁻¹ * 1 : by simp only [mul_one]
... = (a⁻¹)⁻¹ * (a⁻¹ * a) : by simp only [inv_mul_self]
... = ((a⁻¹)⁻¹ * a⁻¹) * a : by simp only [mul_assoc]
... = 1 * a : by simp only [inv_mul_self]
... = a : by simp only [one_mul]
-- 3ª demostración
-- ===============
example : (a⁻¹)⁻¹ = a :=
calc (a⁻¹)⁻¹
= (a⁻¹)⁻¹ * 1 : by simp
... = (a⁻¹)⁻¹ * (a⁻¹ * a) : by simp
... = ((a⁻¹)⁻¹ * a⁻¹) * a : by simp
... = 1 * a : by simp
... = a : by simp
-- 4ª demostración
-- ===============
example : (a⁻¹)⁻¹ = a :=
begin
apply mul_eq_one_iff_inv_eq.mp,
exact mul_left_inv a,
end
-- 5ª demostración
-- ===============
example : (a⁻¹)⁻¹ = a :=
mul_eq_one_iff_inv_eq.mp (mul_left_inv a)
-- 6ª demostración
-- ===============
example : (a⁻¹)⁻¹ = a:=
inv_inv a
-- 7ª demostración
-- ===============
example : (a⁻¹)⁻¹ = a:=
by simp
-- Referencia
-- ==========
-- Propiedad 3.20 del libro "Abstract algebra: Theory and applications"
-- de Thomas W. Judson.
-- http://abstract.ups.edu/download/aata-20200730.pdf#page=49