Inverso_del_producto.md

title	date	category	has_math
Si G es un grupo y a, b ∈ G, entonces (ab)⁻¹ = b⁻¹a⁻¹	2024-05-14 06:00:00 UTC+02:00	Grupos	true

[mathjax]

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

[mathjax] 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]} \\ &= a·((b·b⁻¹)·a⁻¹) &&\text{[por la asociativa]} \\ &= a·(1·a⁻¹) &&\text{[por producto con inverso]} \\ &= a·a⁻¹ &&\text{[por producto con uno]} \\ &= 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_right_inv]
  _ = a * a⁻¹               := by rw [one_mul]
  _ = 1                     := by rw [mul_right_inv]

-- 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

-- 3ª 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]

-- 4ª demostración
example : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
by
  have h1 : (a * b) * (b⁻¹ * a⁻¹) = 1 :=
    aux a b
  simp [h1]

-- 5ª demostración
example : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
by
  apply inv_eq_of_mul_eq_one_right
  rw [aux]

-- 6ª demostración
example : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
by exact mul_inv_rev a b

-- 7ª demostración
example : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
by simp

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

• J. Avigad y P. Massot. Mathematics in Lean, p. 12.