Skip to main content

Si G es un grupo y a, b ∈ G, entonces (ab)⁻¹ = b⁻¹a⁻¹

Demostrar con Lean4 que si \(G\) es un grupo y \(a, b \in G\), entonces \((ab)^{-1} = b^{-1}a^{-1}\).

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

import Mathlib.Algebra.Group.Defs

variable {G : Type _} [Group G]
variable (a b : G)

example : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
sorry

Demostración en lenguaje natural

Teniendo en cuenta la propiedad \[(∀ a, b ∈ G)[ab = 1 → a⁻¹ = b] \] basta demostrar que \[(a·b)·(b⁻¹·a⁻¹) = 1.\] que se demuestra mediante la siguiente cadena de igualdades \begin{align} (a·b)·(b⁻¹·a⁻¹) &= a·(b·(b⁻¹·a⁻¹)) &&\text{[por la asociativa]} \newline &= a·((b·b⁻¹)·a⁻¹) &&\text{[por la asociativa]} \newline &= a·(1·a⁻¹) &&\text{[por producto con inverso]} \newline &= a·a⁻¹ &&\text{[por producto con uno]} \newline &= 1 &&\text{[por producto con inverso]} \end{align}

Demostraciones con Lean4

import Mathlib.Algebra.Group.Defs

variable {G : Type _} [Group G]
variable (a b : G)

lemma aux : (a * b) * (b⁻¹ * a⁻¹) = 1 :=
calc
  (a * b) * (b⁻¹ * a⁻¹)
    = a * (b * (b⁻¹ * a⁻¹)) := by rw [mul_assoc]
  _ = a * ((b * b⁻¹) * a⁻¹) := by rw [mul_assoc]
  _ = a * (1 * a⁻¹)         := by rw [mul_inv_cancel]
  _ = a * a⁻¹               := by rw [one_mul]
  _ = 1                     := by rw [mul_inv_cancel]

-- 1ª demostración
-- ===============

example : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
by
  have h1 : (a * b) * (b⁻¹ * a⁻¹) = 1 :=
    aux a b
  show (a * b)⁻¹ = b⁻¹ * a⁻¹
  exact inv_eq_of_mul_eq_one_right h1

-- 2ª demostración
-- ===============

example : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
by
  have h1 : (a * b) * (b⁻¹ * a⁻¹) = 1 :=
    aux a b
  show (a * b)⁻¹ = b⁻¹ * a⁻¹
  simp [h1]

-- 3ª demostración
-- ===============

example : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
by
  have h1 : (a * b) * (b⁻¹ * a⁻¹) = 1 :=
    aux a b
  simp [h1]

-- 4ª demostración
-- ===============

example : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
by
  apply inv_eq_of_mul_eq_one_right
  rw [aux]

-- 5ª demostración
-- ===============

example : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
by exact mul_inv_rev a b

-- 6ª demostración
-- ===============

example : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
by simp

-- Lemas usados
-- ============

-- variable (c : G)
-- #check (inv_eq_of_mul_eq_one_right : a * b = 1 → a⁻¹ = b)
-- #check (mul_assoc a b c : (a * b) * c = a * (b * c))
-- #check (mul_inv_cancel a : a * a⁻¹ = 1)
-- #check (mul_inv_rev a b : (a * b)⁻¹ = b⁻¹ * a⁻¹)
-- #check (one_mul a : 1 * a = a)

Se puede interactuar con las demostraciones anteriores en Lean 4 Web.

3. Demostraciones con Isabelle/HOL

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)

end

end

Referencias