Menu Close

DAO: La semana en Calculemus (16 de septiembre de 2022)

Esta semana he publicado en Calculemus las demostraciones con Lean de las siguientes propiedades:

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

a - b = a + -b

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

import algebra.ring
 
variables {R : Type*} [ring R]
variables {a b : R}
 
example : a - b = a + -b :=
sorry

Soluciones con Lean

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

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

2 * a = a + a.

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

import algebra.ring
 
variables {R : Type*} [ring R]
variables a : R
 
example : 2 * a = a + a :=
sorry

Soluciones con Lean

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

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

   variables {G : Type*} [group G]

y, como consecuencia, se tiene los siguientes axiomas

   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

a * a⁻¹ = 1

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

import algebra.group
variables {G : Type*} [group G]
variables (a b : G)
 
example : a * a⁻¹ = 1 :=
sorry

Soluciones con Lean

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

4. Si G es un grupo y a ∈ G, entonces a * 1 = a

Demostrar que si G es un grupo y a ∈ G, entonces

a * 1 = a

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

import algebra.group
variables {G : Type*} [group G]
variables a : G
 
example : a * 1 = a :=
sorry

Soluciones con Lean

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

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

b * a = 1

entonces

a⁻¹ = b

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

import algebra.group
variables {G : Type*} [group G]
variables a b : G
 
example
  (h : b * a = 1)
  : a⁻¹ = b :=
sorry

Soluciones con Lean

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

ForMatUS