DAO: La semana en Calculemus (16 de septiembre de 2022)
Esta semana he publicado en Calculemus las demostraciones con Lean de las siguientes propiedades:
- 1. Si R es un anillo y a, b ∈ R, entonces a – b = a + -b
- 2. Si R es un anillo y a ∈ R, entonces 2 * a = a + a
- 3. Si G es un grupo y a ∈ G, entonces a * a⁻¹ = 1
- 4. Si G es un grupo y a ∈ G, entonces a * 1 = a
- 5. Si G es un grupo y a, b ∈ G tales que b * a = 1, entonces a⁻¹ = b
A continuación se muestran las soluciones.
1. Si R es un anillo y a, b ∈ R, entonces a – b = a + -b
Demostrar que si R es un anillo y a, b ∈ R, entonces
|
1 |
a - b = a + -b |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 |
import algebra.ring variables {R : Type*} [ring R] variables {a b : R} example : a - b = a + -b := sorry |
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 |
import algebra.ring variables {R : Type*} [ring R] variables {a b : R} -- 1ª demostración -- =============== example : a - b = a + -b := begin apply sub_eq_iff_eq_add.mpr, calc a = a + 0 : (add_zero a).symm ... = a + (-b + b) : congr_arg (λ x, a + x) (neg_add_self b).symm ... = a + -b + b : (add_assoc a (-b) b).symm end -- 2ª demostración -- =============== example : a - b = a + -b := begin apply sub_eq_iff_eq_add.mpr, calc a = a + 0 : by rw add_zero ... = a + (-b + b) : by {congr; rw neg_add_self} ... = a + -b + b : by rw add_assoc end -- 3ª demostración -- =============== example : a - b = a + -b := begin rw sub_eq_iff_eq_add, rw add_assoc, rw neg_add_self, rw add_zero, end -- 4ª demostración -- =============== example : a - b = a + -b := by rw [sub_eq_iff_eq_add, add_assoc, neg_add_self, add_zero] -- 5ª demostración -- =============== example : a - b = a + -b := by simp [sub_eq_iff_eq_add] -- 6ª demostración -- =============== example : a - b = a + -b := -- by library_search sub_eq_add_neg a b |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
Referencias
- J. Avigad, K. Buzzard, R.Y. Lewis y P. Massot. Mathematics in Lean, p. 13.
2. Si R es un anillo y a ∈ R, entonces 2 * a = a + a
Demostrar que si R es un anillo y a ∈ R, entonces
|
1 |
2 * a = a + a. |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 |
import algebra.ring variables {R : Type*} [ring R] variables a : R example : 2 * a = a + a := sorry |
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 |
import algebra.ring variables {R : Type*} [ring R] variables a : R -- 1ª demostración -- =============== example : 2 * a = a + a := calc 2 * a = (1 + 1) * a : congr_fun (congr_arg has_mul.mul one_add_one_eq_two.symm) a ... = 1 * a + 1 * a : add_mul 1 1 a ... = a + 1 * a : congr_arg (λ x, x + 1 * a) (one_mul a) ... = a + a : congr_arg (λ x, a + x) (one_mul a) -- 2ª demostración -- =============== example : 2 * a = a + a := calc 2 * a = (1 + 1) * a : by rw one_add_one_eq_two ... = 1 * a + 1 * a : by rw add_mul ... = a + a : by rw one_mul -- 3ª demostración -- =============== example : 2 * a = a + a := by rw [one_add_one_eq_two.symm, add_mul, one_mul] -- 4ª demostración -- =============== example : 2 * a = a + a := calc 2 * a = (1 + 1) * a : rfl ... = 1 * a + 1 * a : by simp [add_mul] ... = a + a : by simp -- 5ª demostración -- =============== example : 2 * a = a + a := -- by library_search two_mul a |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
Referencias
- J. Avigad, K. Buzzard, R.Y. Lewis y P. Massot. Mathematics in Lean, p. 13.
3. Si G es un grupo y a ∈ G, entonces a * a⁻¹ = 1
En Lean, se declara que G es un grupo mediante la expresión
|
1 |
variables {G : Type*} [group G] |
y, como consecuencia, se tiene los siguientes axiomas
|
1 2 3 |
mul_assoc : ∀ a b c : G, a * b * c = a * (b * c) one_mul : ∀ a : G, 1 * a = a mul_left_inv : ∀ a : G, a⁻¹ * a = 1 |
Demostrar que si G es un grupo y a ∈ G, entonces
|
1 |
a * a⁻¹ = 1 |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 |
import algebra.group variables {G : Type*} [group G] variables (a b : G) example : a * a⁻¹ = 1 := sorry |
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 |
import algebra.group variables {G : Type*} [group G] variables (a b : G) -- 1ª demostración -- =============== example : a * a⁻¹ = 1 := calc a * a⁻¹ = 1 * (a * a⁻¹) : (one_mul (a * a⁻¹)).symm ... = (1 * a) * a⁻¹ : (mul_assoc 1 a a⁻¹).symm ... = (((a⁻¹)⁻¹ * a⁻¹) * a) * a⁻¹ : congr_arg (λ x, (x * a) * a⁻¹) (mul_left_inv a⁻¹).symm ... = ((a⁻¹)⁻¹ * (a⁻¹ * a)) * a⁻¹ : congr_fun (congr_arg has_mul.mul (mul_assoc a⁻¹⁻¹ a⁻¹ a)) a⁻¹ ... = ((a⁻¹)⁻¹ * 1) * a⁻¹ : congr_arg (λ x, (a⁻¹⁻¹ * x) * a⁻¹) (mul_left_inv a) ... = (a⁻¹)⁻¹ * (1 * a⁻¹) : mul_assoc (a⁻¹)⁻¹ 1 a⁻¹ ... = (a⁻¹)⁻¹ * a⁻¹ : congr_arg (λ x, (a⁻¹)⁻¹ * x) (one_mul a⁻¹) ... = 1 : mul_left_inv a⁻¹ -- 2ª demostración -- =============== example : a * a⁻¹ = 1 := calc a * a⁻¹ = 1 * (a * a⁻¹) : by rw one_mul ... = (1 * a) * a⁻¹ : by rw mul_assoc ... = (((a⁻¹)⁻¹ * a⁻¹) * a) * a⁻¹ : by rw mul_left_inv ... = ((a⁻¹)⁻¹ * (a⁻¹ * a)) * a⁻¹ : by rw ← mul_assoc ... = ((a⁻¹)⁻¹ * 1) * a⁻¹ : by rw mul_left_inv ... = (a⁻¹)⁻¹ * (1 * a⁻¹) : by rw mul_assoc ... = (a⁻¹)⁻¹ * a⁻¹ : by rw one_mul ... = 1 : by rw mul_left_inv -- 3ª demostración -- =============== example : a * a⁻¹ = 1 := calc a * a⁻¹ = 1 * (a * a⁻¹) : by simp ... = (1 * a) * a⁻¹ : by simp ... = (((a⁻¹)⁻¹ * a⁻¹) * a) * a⁻¹ : by simp ... = ((a⁻¹)⁻¹ * (a⁻¹ * a)) * a⁻¹ : by simp ... = ((a⁻¹)⁻¹ * 1) * a⁻¹ : by simp ... = (a⁻¹)⁻¹ * (1 * a⁻¹) : by simp ... = (a⁻¹)⁻¹ * a⁻¹ : by simp ... = 1 : by simp -- 4ª demostración -- =============== example : a * a⁻¹ = 1 := by simp -- 5ª demostración -- =============== example : a * a⁻¹ = 1 := -- by library_search mul_inv_self a |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
Referencias
- J. Avigad, K. Buzzard, R.Y. Lewis y P. Massot. Mathematics in Lean, p. 14.
4. Si G es un grupo y a ∈ G, entonces a * 1 = a
Demostrar que si G es un grupo y a ∈ G, entonces
|
1 |
a * 1 = a |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 |
import algebra.group variables {G : Type*} [group G] variables a : G example : a * 1 = a := sorry |
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 |
import algebra.group variables {G : Type*} [group G] variables a : G -- 1ª demostración -- =============== example : a * 1 = a := calc a * 1 = a * (a⁻¹ * a) : congr_arg (λ x, a * x) (mul_left_inv a).symm ... = (a * a⁻¹) * a : (mul_assoc a a⁻¹ a).symm ... = 1 * a : congr_arg (λ x, x* a) (mul_right_inv a) ... = a : one_mul a -- 2ª demostración -- =============== example : a * 1 = a := calc a * 1 = a * (a⁻¹ * a) : by rw mul_left_inv ... = (a * a⁻¹) * a : by rw mul_assoc ... = 1 * a : by rw mul_right_inv ... = a : by rw one_mul -- 3ª demostración -- =============== example : a * 1 = a := calc a * 1 = a * (a⁻¹ * a) : by simp ... = (a * a⁻¹) * a : by simp ... = 1 * a : by simp ... = a : by simp -- 3ª demostración -- =============== example : a * 1 = a := by simp -- 4ª demostración -- =============== example : a * 1 = a := -- by library_search mul_one a |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
Referencias
- J. Avigad, K. Buzzard, R.Y. Lewis y P. Massot. Mathematics in Lean, p. 14.
5. Si G es un grupo y a, b ∈ G tales que b * a = 1, entonces a⁻¹ = b
Demostrar que si G es un grupo y a, b ∈ G tales que
|
1 |
b * a = 1 |
entonces
|
1 |
a⁻¹ = b |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 |
import algebra.group variables {G : Type*} [group G] variables a b : G example (h : b * a = 1) : a⁻¹ = b := sorry |
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 |
import algebra.group variables {G : Type*} [group G] variables a b : G -- 1ª demostración -- =============== example (h : b * a = 1) : a⁻¹ = b := calc a⁻¹ = 1 * a⁻¹ : (one_mul a⁻¹).symm ... = (b * a) * a⁻¹ : congr_arg (λ x, x * a⁻¹) h.symm ... = b * (a * a⁻¹) : mul_assoc b a a⁻¹ ... = b * 1 : congr_arg (λ x, b * x) (mul_right_inv a) ... = b : mul_one b -- 2ª demostración -- =============== example (h : b * a = 1) : a⁻¹ = b := calc a⁻¹ = 1 * a⁻¹ : by rw one_mul ... = (b * a) * a⁻¹ : by rw h ... = b * (a * a⁻¹) : by rw mul_assoc ... = b * 1 : by rw mul_right_inv ... = b : by rw mul_one -- 3ª demostración -- =============== example (h : b * a = 1) : a⁻¹ = b := calc a⁻¹ = 1 * a⁻¹ : by simp ... = (b * a) * a⁻¹ : by simp [h] ... = b * (a * a⁻¹) : by simp ... = b * 1 : by simp ... = b : by simp -- 4ª demostración -- =============== example (h : b * a = 1) : a⁻¹ = b := -- by library_search inv_eq_of_mul_eq_one_left h |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
Referencias
- J. Avigad, K. Buzzard, R.Y. Lewis y P. Massot. Mathematics in Lean.