julio 2021 – Página 3

Límite de sucesiones constantes

PorJosé A. Alonso 11 julio 20214 julio 2021

En Lean, una sucesión u₀, u₁, u₂, … se puede representar mediante una función (u : ℕ → ℝ) de forma que u(n) es uₙ.

Se define que a es el límite de la sucesión u, por

   def limite : (ℕ → ℝ) → ℝ → Prop :=
   λ u a, ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - a| < ε

1 2	def limite : (ℕ → ℝ) → ℝ → Prop := λ u a, ∀ ε > 0, ∃ N, ∀ n ≥ N, \|u n - a\| < ε

donde se usa la notación |x| para el valor absoluto de x

   notation `|`x`|` := abs x

1	notation `\|`x`\|` := abs x

Demostrar que el límite de la sucesión constante c es c.

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

import data.real.basic

variable (u : ℕ → ℝ)
variable (c : ℝ)

notation `|`x`|` := abs x

def limite : (ℕ → ℝ) → ℝ → Prop :=
λ u a, ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - a| < ε

example :
  limite (λ n, c) c :=
sorry

import data.real.basic

variable (u : ℕ → ℝ)

variable (c : ℝ)

notation `|`x`|` := abs x

def limite : (ℕ → ℝ) → ℝ → Prop :=

λ u a, ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - a| < ε

example :

limite (λ n, c) c :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic

variable (u : ℕ → ℝ)
variable (c : ℝ)

notation `|`x`|` := abs x

def limite : (ℕ → ℝ) → ℝ → Prop :=
λ u a, ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - a| < ε

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

example :
  limite (λ n, c) c :=
begin
  unfold limite,
  intros ε hε,
  use 0,
  intros n hn,
  dsimp,
  simp,
  exact hε,
end

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

example :
  limite (λ n, c) c :=
begin
  intros ε hε,
  use 0,
  rintro n -,
  norm_num,
  assumption,
end

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

example :
  limite (λ n, c) c :=
begin
  intros ε hε,
  use 0,
  intros n hn,
  calc |(λ n, c) n - c|
       = |c - c|  : rfl
   ... = 0        : by simp
   ... < ε        : hε
end

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

example :
  limite (λ n, c) c :=
begin
  intros ε hε,
  by finish,
end

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

example :
  limite (λ n, c) c :=
λ ε hε, by finish

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

example :
  limite (λ n, c) c :=
assume ε,
assume hε : ε > 0,
exists.intro 0
  ( assume n,
    assume hn : n ≥ 0,
    show |(λ n, c) n - c| < ε, from
      calc |(λ n, c) n - c|
           = |c - c|  : rfl
       ... = 0        : by simp
       ... < ε        : hε)

import data.real.basic

variable (u : ℕ → ℝ)

variable (c : ℝ)

notation `|`x`|` := abs x

def limite : (ℕ → ℝ) → ℝ → Prop :=

λ u a, ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - a| < ε

-- 1ª demostración

-- ===============

example :

limite (λ n, c) c :=

begin

unfold limite,

intros ε hε,

use 0,

intros n hn,

dsimp,

simp,

exact hε,

end

-- 2ª demostración

-- ===============

example :

limite (λ n, c) c :=

begin

intros ε hε,

use 0,

rintro n -,

norm_num,

assumption,

end

-- 3ª demostración

-- ===============

example :

limite (λ n, c) c :=

begin

intros ε hε,

use 0,

intros n hn,

calc |(λ n, c) n - c|

= |c - c| : rfl

... = 0 : by simp

... < ε : hε

end

-- 4ª demostración

-- ===============

example :

limite (λ n, c) c :=

begin

intros ε hε,

by finish,

end

-- 5ª demostración

-- ===============

example :

limite (λ n, c) c :=

λ ε hε, by finish

-- 6ª demostración

-- ===============

example :

limite (λ n, c) c :=

assume ε,

assume hε : ε > 0,

exists.intro 0

( assume n,

assume hn : n ≥ 0,

show |(λ n, c) n - c| < ε, from

calc |(λ n, c) n - c|

= |c - c| : rfl

... = 0 : by simp

... < ε : hε)

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

(* ---------------------------------------------------------------------
-- En Isabelle/HOL, una sucesión u₀, u₁, u₂, ... se puede representar 
-- mediante una función (u : ℕ → ℝ) de forma que u(n) es uₙ.
--
-- Se define que a es el límite de la sucesión u, por
--    definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool"
--      where "limite u c ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦u n - c¦ < ε)"
--
-- Demostrar que el límite de la sucesión constante c es c.
-- ------------------------------------------------------------------ *)

theory Limite_de_sucesiones_constantes
imports Main HOL.Real
begin

definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool"
  where "limite u c ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦u n - c¦ < ε)"

(* 1ª demostración *)

lemma "limite (λ n. c) c"
proof (unfold limite_def)
  show "∀ε>0. ∃k::nat. ∀n≥k. ¦c - c¦ < ε" 
  proof (intro allI impI)
    fix ε :: real
    assume "0 < ε"
    have "∀n≥0::nat. ¦c - c¦ < ε" 
    proof (intro allI impI)
      fix n :: nat
      assume "0 ≤ n"
      have "c - c = 0" 
        by (simp only: diff_self)
      then have "¦c - c¦ = 0" 
        by (simp only: abs_eq_0_iff)
      also have "… < ε"
        by (simp only: ‹0 < ε›) 
      finally show "¦c - c¦ < ε" 
        by this
    qed
    then show "∃k::nat. ∀n≥k. ¦c - c¦ < ε" 
      by (rule exI)
  qed
qed

(* 2ª demostración *)

lemma "limite (λ n. c) c"
proof (unfold limite_def)
  show "∀ε>0. ∃k::nat. ∀n≥k. ¦c - c¦ < ε" 
  proof (intro allI impI)
    fix ε :: real
    assume "0 < ε"
    have "∀n≥0::nat. ¦c - c¦ < ε"          by (simp add: ‹0 < ε›)   
    then show "∃k::nat. ∀n≥k. ¦c - c¦ < ε" by (rule exI)
  qed
qed

(* 3ª demostración *)

lemma "limite (λ n. c) c" 
  unfolding limite_def
  by simp

(* 4ª demostración *)

lemma "limite (λ n. c) c" 
  by (simp add: limite_def)

end

(* ---------------------------------------------------------------------

-- En Isabelle/HOL, una sucesión u₀, u₁, u₂, ... se puede representar

-- mediante una función (u : ℕ → ℝ) de forma que u(n) es uₙ.

-- Se define que a es el límite de la sucesión u, por

-- definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool"

-- where "limite u c ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦u n - c¦ < ε)"

-- Demostrar que el límite de la sucesión constante c es c.

-- ------------------------------------------------------------------ *)

theory Limite_de_sucesiones_constantes

imports Main HOL.Real

begin

definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool"

where "limite u c ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦u n - c¦ < ε)"

(* 1ª demostración *)

lemma "limite (λ n. c) c"

proof (unfold limite_def)

show "∀ε>0. ∃k::nat. ∀n≥k. ¦c - c¦ < ε"

proof (intro allI impI)

fix ε :: real

assume "0 < ε"

have "∀n≥0::nat. ¦c - c¦ < ε"

proof (intro allI impI)

fix n :: nat

assume "0 ≤ n"

have "c - c = 0"

by (simp only: diff_self)

then have "¦c - c¦ = 0"

by (simp only: abs_eq_0_iff)

also have "… < ε"

by (simp only: ‹0 < ε›)

finally show "¦c - c¦ < ε"

by this

qed

then show "∃k::nat. ∀n≥k. ¦c - c¦ < ε"

by (rule exI)

qed

(* 2ª demostración *)

lemma "limite (λ n. c) c"

proof (unfold limite_def)

show "∀ε>0. ∃k::nat. ∀n≥k. ¦c - c¦ < ε"

proof (intro allI impI)

fix ε :: real

assume "0 < ε"

have "∀n≥0::nat. ¦c - c¦ < ε" by (simp add: ‹0 < ε›)

then show "∃k::nat. ∀n≥k. ¦c - c¦ < ε" by (rule exI)

qed

(* 3ª demostración *)

lemma "limite (λ n. c) c"

unfolding limite_def

by simp

(* 4ª demostración *)

lemma "limite (λ n. c) c"

by (simp add: limite_def)

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Los monoides booleanos son conmutativos

PorJosé A. Alonso 10 julio 20214 julio 2021

Un monoide es un conjunto junto con una operación binaria que es asociativa y tiene elemento neutro.

Un monoide M es booleano si

   ∀ x ∈ M, x * x = 1

1	∀ x ∈ M, x * x = 1

y es conmutativo si

   ∀ x y ∈ M, x * y = y * x

1	∀ x y ∈ M, x * y = y * x

En Lean, está definida la clase de los monoides (como monoid) y sus propiedades características son

   mul_assoc : (a * b) * c = a * (b * c)
   one_mul :   1 * a = a
   mul_one :   a * 1 = a

mul_assoc : (a * b) * c = a * (b * c)

one_mul : 1 * a = a

mul_one : a * 1 = a

Demostrar que los monoides booleanos son conmutativos.

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

import algebra.group.basic

universe  u
variables {M : Type u} [monoid M]

example
  (h : ∀ x : M, x * x = 1)
  : ∀ x y : M, x * y = y * x :=
sorry

import algebra.group.basic

universe u

variables {M : Type u} [monoid M]

example

(h : ∀ x : M, x * x = 1)

: ∀ x y : M, x * y = y * x :=

sorry

[expand title=»Soluciones con Lean»]

import algebra.group.basic

universe  u
variables {M : Type u} [monoid M]

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

example
  (h : ∀ x : M, x * x = 1)
  : ∀ x y : M, x * y = y * x :=
begin
  intros a b,
  calc a * b
       = (a * b) * 1                   : (mul_one (a * b)).symm
   ... = (a * b) * (a * a)             : congr_arg ((*) (a*b)) (h a).symm
   ... = ((a * b) * a) * a             : (mul_assoc (a*b) a a).symm
   ... = (a * (b * a)) * a             : congr_arg (* a) (mul_assoc a b a)
   ... = (1 * (a * (b * a))) * a       : congr_arg (* a) (one_mul (a*(b*a))).symm
   ... = ((b * b) * (a * (b * a))) * a : congr_arg (* a) (congr_arg (* (a*(b*a))) (h b).symm)
   ... = (b * (b * (a * (b * a)))) * a : congr_arg (* a) (mul_assoc b b (a*(b*a)))
   ... = (b * ((b * a) * (b * a))) * a : congr_arg (* a) (congr_arg ((*) b) (mul_assoc b a (b*a)).symm)
   ... = (b * 1) * a                   : congr_arg (* a) (congr_arg ((*) b) (h (b*a)))
   ... = b * a                         : congr_arg (* a) (mul_one b),
end

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

example
  (h : ∀ x : M, x * x = 1)
  : ∀ x y : M, x * y = y * x :=
begin
  intros a b,
  calc a * b
       = (a * b) * 1                   : by simp only [mul_one]
   ... = (a * b) * (a * a)             : by simp only [h]
   ... = ((a * b) * a) * a             : by simp only [mul_assoc]
   ... = (a * (b * a)) * a             : by simp only [mul_assoc]
   ... = (1 * (a * (b * a))) * a       : by simp only [one_mul]
   ... = ((b * b) * (a * (b * a))) * a : by simp only [h]
   ... = (b * (b * (a * (b * a)))) * a : by simp only [mul_assoc]
   ... = (b * ((b * a) * (b * a))) * a : by simp only [mul_assoc]
   ... = (b * 1) * a                   : by simp only [h]
   ... = b * a                         : by simp only [mul_one]
end

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

example
  (h : ∀ x : M, x * x = 1)
  : ∀ x y : M, x * y = y * x :=
begin
  intros a b,
  calc a * b
       = (a * b) * 1                   : by simp
   ... = (a * b) * (a * a)             : by simp [h]
   ... = ((a * b) * a) * a             : by simp [mul_assoc]
   ... = (a * (b * a)) * a             : by simp [mul_assoc]
   ... = (1 * (a * (b * a))) * a       : by simp
   ... = ((b * b) * (a * (b * a))) * a : by simp [h]
   ... = (b * (b * (a * (b * a)))) * a : by simp [mul_assoc]
   ... = (b * ((b * a) * (b * a))) * a : by simp [mul_assoc]
   ... = (b * 1) * a                   : by simp [h]
   ... = b * a                         : by simp,
end

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

example
  (h : ∀ x : M, x * x = 1)
  : ∀ x y : M, x * y = y * x :=
begin
  intros a b,
  calc a * b
       = (a * b) * (a * a)             : by simp [h]
   ... = (1 * (a * (b * a))) * a       : by simp [mul_assoc]
   ... = ((b * b) * (a * (b * a))) * a : by simp [h]
   ... = (b * ((b * a) * (b * a))) * a : by simp [mul_assoc]
   ... = b * a                         : by simp [h],
end

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

example
  (h : ∀ x : M, x * x = 1)
  : ∀ x y : M, x * y = y * x :=
begin
  intros a b,
  calc a * b
       = ((b * b) * (a * (b * a))) * a : by simp [h, mul_assoc]
   ... = (b * ((b * a) * (b * a))) * a : by simp [mul_assoc]
   ... = b * a                         : by simp [h],
end

import algebra.group.basic

universe u

variables {M : Type u} [monoid M]

-- 1ª demostración

-- ===============

example

(h : ∀ x : M, x * x = 1)

: ∀ x y : M, x * y = y * x :=

begin

intros a b,

calc a * b

= (a * b) * 1 : (mul_one (a * b)).symm

... = (a * b) * (a * a) : congr_arg ((*) (a*b)) (h a).symm

... = ((a * b) * a) * a : (mul_assoc (a*b) a a).symm

... = (a * (b * a)) * a : congr_arg (* a) (mul_assoc a b a)

... = (1 * (a * (b * a))) * a : congr_arg (* a) (one_mul (a*(b*a))).symm

... = ((b * b) * (a * (b * a))) * a : congr_arg (* a) (congr_arg (* (a*(b*a))) (h b).symm)

... = (b * (b * (a * (b * a)))) * a : congr_arg (* a) (mul_assoc b b (a*(b*a)))

... = (b * ((b * a) * (b * a))) * a : congr_arg (* a) (congr_arg ((*) b) (mul_assoc b a (b*a)).symm)

... = (b * 1) * a : congr_arg (* a) (congr_arg ((*) b) (h (b*a)))

... = b * a : congr_arg (* a) (mul_one b),

end

-- 2ª demostración

-- ===============

example

(h : ∀ x : M, x * x = 1)

: ∀ x y : M, x * y = y * x :=

begin

intros a b,

calc a * b

= (a * b) * 1 : by simp only [mul_one]

... = (a * b) * (a * a) : by simp only [h]

... = ((a * b) * a) * a : by simp only [mul_assoc]

... = (a * (b * a)) * a : by simp only [mul_assoc]

... = (1 * (a * (b * a))) * a : by simp only [one_mul]

... = ((b * b) * (a * (b * a))) * a : by simp only [h]

... = (b * (b * (a * (b * a)))) * a : by simp only [mul_assoc]

... = (b * ((b * a) * (b * a))) * a : by simp only [mul_assoc]

... = (b * 1) * a : by simp only [h]

... = b * a : by simp only [mul_one]

end

-- 3ª demostración

-- ===============

example

(h : ∀ x : M, x * x = 1)

: ∀ x y : M, x * y = y * x :=

begin

intros a b,

calc a * b

= (a * b) * 1 : by simp

... = (a * b) * (a * a) : by simp [h]

... = ((a * b) * a) * a : by simp [mul_assoc]

... = (a * (b * a)) * a : by simp [mul_assoc]

... = (1 * (a * (b * a))) * a : by simp

... = ((b * b) * (a * (b * a))) * a : by simp [h]

... = (b * (b * (a * (b * a)))) * a : by simp [mul_assoc]

... = (b * ((b * a) * (b * a))) * a : by simp [mul_assoc]

... = (b * 1) * a : by simp [h]

... = b * a : by simp,

end

-- 4ª demostración

-- ===============

example

(h : ∀ x : M, x * x = 1)

: ∀ x y : M, x * y = y * x :=

begin

intros a b,

calc a * b

= (a * b) * (a * a) : by simp [h]

... = (1 * (a * (b * a))) * a : by simp [mul_assoc]

... = ((b * b) * (a * (b * a))) * a : by simp [h]

... = (b * ((b * a) * (b * a))) * a : by simp [mul_assoc]

... = b * a : by simp [h],

end

-- 5ª demostración

-- ===============

example

(h : ∀ x : M, x * x = 1)

: ∀ x y : M, x * y = y * x :=

begin

intros a b,

calc a * b

= ((b * b) * (a * (b * a))) * a : by simp [h, mul_assoc]

... = (b * ((b * a) * (b * a))) * a : by simp [mul_assoc]

... = b * a : by simp [h],

end

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory Los_monoides_booleanos_son_conmutativos
imports Main
begin

context monoid
begin

(* 1ª demostración *)

lemma
  assumes "∀ x. x * x = 1"
  shows   "∀ x y. x * y = y * x"
proof (rule allI)+
  fix a b
  have "a * b = (a * b) * 1"
    by (simp only: right_neutral)
  also have "… = (a * b) * (a * a)"
    by (simp only: assms)
  also have "… = ((a * b) * a) * a"
    by (simp only: assoc)
  also have "… = (a * (b * a)) * a"
    by (simp only: assoc)
  also have "… = (1 * (a * (b * a))) * a"
    by (simp only: left_neutral)
  also have "… = ((b * b) * (a * (b * a))) * a"
    by (simp only: assms)
  also have "… = (b * (b * (a * (b * a)))) * a"
    by (simp only: assoc)
  also have "… = (b * ((b * a) * (b * a))) * a"
    by (simp only: assoc)
  also have "… = (b * 1) * a"
    by (simp only: assms)
  also have "… = b * a"
    by (simp only: right_neutral)
  finally show "a * b = b * a"
    by this
qed

(* 2ª demostración *)

lemma
  assumes "∀ x. x * x = 1"
  shows   "∀ x y. x * y = y * x"
proof (rule allI)+
  fix a b
  have "a * b = (a * b) * 1"                    by simp
  also have "… = (a * b) * (a * a)"             by (simp add: assms)
  also have "… = ((a * b) * a) * a"             by (simp add: assoc)
  also have "… = (a * (b * a)) * a"             by (simp add: assoc)
  also have "… = (1 * (a * (b * a))) * a"       by simp
  also have "… = ((b * b) * (a * (b * a))) * a" by (simp add: assms)
  also have "… = (b * (b * (a * (b * a)))) * a" by (simp add: assoc)
  also have "… = (b * ((b * a) * (b * a))) * a" by (simp add: assoc)
  also have "… = (b * 1) * a"                   by (simp add: assms)
  also have "… = b * a"                         by simp
  finally show "a * b = b * a"                  by this
qed

(* 3ª demostración *)

lemma
  assumes "∀ x. x * x = 1"
  shows   "∀ x y. x * y = y * x"
proof (rule allI)+
  fix a b
  have "a * b = (a * b) * (a * a)"              by (simp add: assms)
  also have "… = (a * (b * a)) * a"             by (simp add: assoc)
  also have "… = ((b * b) * (a * (b * a))) * a" by (simp add: assms)
  also have "… = (b * ((b * a) * (b * a))) * a" by (simp add: assoc)
  also have "… = (b * 1) * a"                   by (simp add: assms)
  finally show "a * b = b * a"                  by simp
qed

(* 4ª demostración *)

lemma
  assumes "∀ x. x * x = 1"
  shows   "∀ x y. x * y = y * x"
  by (metis assms assoc right_neutral)

end

end

theory Los_monoides_booleanos_son_conmutativos

imports Main

begin

context monoid

begin

(* 1ª demostración *)

lemma

assumes "∀ x. x * x = 1"

shows "∀ x y. x * y = y * x"

proof (rule allI)+

fix a b

have "a * b = (a * b) * 1"

by (simp only: right_neutral)

also have "… = (a * b) * (a * a)"

by (simp only: assms)

also have "… = ((a * b) * a) * a"

by (simp only: assoc)

also have "… = (a * (b * a)) * a"

by (simp only: assoc)

also have "… = (1 * (a * (b * a))) * a"

by (simp only: left_neutral)

also have "… = ((b * b) * (a * (b * a))) * a"

by (simp only: assms)

also have "… = (b * (b * (a * (b * a)))) * a"

by (simp only: assoc)

also have "… = (b * ((b * a) * (b * a))) * a"

by (simp only: assoc)

also have "… = (b * 1) * a"

by (simp only: assms)

also have "… = b * a"

by (simp only: right_neutral)

finally show "a * b = b * a"

by this

qed

(* 2ª demostración *)

lemma

assumes "∀ x. x * x = 1"

shows "∀ x y. x * y = y * x"

proof (rule allI)+

fix a b

have "a * b = (a * b) * 1" by simp

also have "… = (a * b) * (a * a)" by (simp add: assms)

also have "… = ((a * b) * a) * a" by (simp add: assoc)

also have "… = (a * (b * a)) * a" by (simp add: assoc)

also have "… = (1 * (a * (b * a))) * a" by simp

also have "… = ((b * b) * (a * (b * a))) * a" by (simp add: assms)

also have "… = (b * (b * (a * (b * a)))) * a" by (simp add: assoc)

also have "… = (b * ((b * a) * (b * a))) * a" by (simp add: assoc)

also have "… = (b * 1) * a" by (simp add: assms)

also have "… = b * a" by simp

finally show "a * b = b * a" by this

qed

(* 3ª demostración *)

lemma

assumes "∀ x. x * x = 1"

shows "∀ x y. x * y = y * x"

proof (rule allI)+

fix a b

have "a * b = (a * b) * (a * a)" by (simp add: assms)

also have "… = (a * (b * a)) * a" by (simp add: assoc)

also have "… = ((b * b) * (a * (b * a))) * a" by (simp add: assms)

also have "… = (b * ((b * a) * (b * a))) * a" by (simp add: assoc)

also have "… = (b * 1) * a" by (simp add: assms)

finally show "a * b = b * a" by simp

qed

(* 4ª demostración *)

lemma

assumes "∀ x. x * x = 1"

shows "∀ x y. x * y = y * x"

by (metis assms assoc right_neutral)

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Potencias de potencias en monoides

PorJosé A. Alonso 9 julio 20214 julio 2021

En los monoides se define la potencia con exponentes naturales. En Lean la potencia x^n se caracteriza por los siguientes lemas:

   pow_zero : x^0 = 1
   pow_succ' : x^(succ n) = x * x^n

1 2	pow_zero : x^0 = 1 pow_succ' : x^(succ n) = x * x^n

Demostrar que si M es un monoide, a ∈ M y m, n ∈ ℕ, entonces

   a^(m * n) = (a^m)^n

1	a^(m * n) = (a^m)^n

Indicación: Se puede usar el lema

   pow_add : a^(m + n) = a^m * a^n

1	pow_add : a^(m + n) = a^m * a^n

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

import algebra.group_power.basic
open monoid nat

variables {M : Type} [monoid M]
variable  a : M
variables (m n : ℕ)

set_option pp.structure_projections false

example : a^(m * n) = (a^m)^n :=
sorry

import algebra.group_power.basic

open monoid nat

variables {M : Type} [monoid M]

variable a : M

variables (m n : ℕ)

set_option pp.structure_projections false

example : a^(m * n) = (a^m)^n :=

sorry

[expand title=»Soluciones con Lean»]

import algebra.group_power.basic
open monoid nat

variables {M : Type} [monoid M]
variable  a : M
variables (m n : ℕ)

-- Para que no use la notación con puntos
set_option pp.structure_projections false

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

example : a^(m * n) = (a^m)^n :=
begin
  induction n with n HI,
  { calc a^(m * 0)
         = a^0             : congr_arg ((^) a) (nat.mul_zero m)
     ... = 1               : pow_zero a
     ... = (a^m)^0         : (pow_zero (a^m)).symm },
  { calc a^(m * succ n)
         = a^(m * n + m)   : congr_arg ((^) a) (nat.mul_succ m n)
     ... = a^(m * n) * a^m : pow_add a (m * n) m
     ... = (a^m)^n * a^m   : congr_arg (* a^m) HI
     ... = (a^m)^(succ n)  : (pow_succ' (a^m) n).symm },
end

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

example : a^(m * n) = (a^m)^n :=
begin
  induction n with n HI,
  { calc a^(m * 0)
         = a^0             : by simp only [nat.mul_zero]
     ... = 1               : by simp only [pow_zero]
     ... = (a^m)^0         : by simp only [pow_zero] },
  { calc a^(m * succ n)
         = a^(m * n + m)   : by simp only [nat.mul_succ]
     ... = a^(m * n) * a^m : by simp only [pow_add]
     ... = (a^m)^n * a^m   : by simp only [HI]
     ... = (a^m)^succ n    : by simp only [pow_succ'] },
end

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

example : a^(m * n) = (a^m)^n :=
begin
  induction n with n HI,
  { calc a^(m * 0)
         = a^0             : by simp [nat.mul_zero]
     ... = 1               : by simp
     ... = (a^m)^0         : by simp },
  { calc a^(m * succ n)
         = a^(m * n + m)   : by simp [nat.mul_succ]
     ... = a^(m * n) * a^m : by simp [pow_add]
     ... = (a^m)^n * a^m   : by simp [HI]
     ... = (a^m)^succ n    : by simp [pow_succ'] },
end

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

example : a^(m * n) = (a^m)^n :=
begin
  induction n with n HI,
  { by simp [nat.mul_zero] },
  { by simp [nat.mul_succ,
             pow_add,
             HI,
             pow_succ'] },
end

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

example : a^(m * n) = (a^m)^n :=
begin
  induction n with n HI,
  { rw nat.mul_zero,
    rw pow_zero,
    rw pow_zero, },
  { rw nat.mul_succ,
    rw pow_add,
    rw HI,
    rw pow_succ', }
end

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

example : a^(m * n) = (a^m)^n :=
begin
  induction n with n HI,
  { rw [nat.mul_zero, pow_zero, pow_zero] },
  { rw [nat.mul_succ, pow_add, HI, pow_succ'] }
end

-- 7ª demostración
-- ===============

example : a^(m * n) = (a^m)^n :=
pow_mul a m n

100

101

102

103

104

import algebra.group_power.basic

open monoid nat

variables {M : Type} [monoid M]

variable a : M

variables (m n : ℕ)

-- Para que no use la notación con puntos

set_option pp.structure_projections false

-- 1ª demostración

-- ===============

example : a^(m * n) = (a^m)^n :=

begin

induction n with n HI,

{ calc a^(m * 0)

= a^0 : congr_arg ((^) a) (nat.mul_zero m)

... = 1 : pow_zero a

... = (a^m)^0 : (pow_zero (a^m)).symm },

{ calc a^(m * succ n)

= a^(m * n + m) : congr_arg ((^) a) (nat.mul_succ m n)

... = a^(m * n) * a^m : pow_add a (m * n) m

... = (a^m)^n * a^m : congr_arg (* a^m) HI

... = (a^m)^(succ n) : (pow_succ' (a^m) n).symm },

end

-- 2ª demostración

-- ===============

example : a^(m * n) = (a^m)^n :=

begin

induction n with n HI,

{ calc a^(m * 0)

= a^0 : by simp only [nat.mul_zero]

... = 1 : by simp only [pow_zero]

... = (a^m)^0 : by simp only [pow_zero] },

{ calc a^(m * succ n)

= a^(m * n + m) : by simp only [nat.mul_succ]

... = a^(m * n) * a^m : by simp only [pow_add]

... = (a^m)^n * a^m : by simp only [HI]

... = (a^m)^succ n : by simp only [pow_succ'] },

end

-- 3ª demostración

-- ===============

example : a^(m * n) = (a^m)^n :=

begin

induction n with n HI,

{ calc a^(m * 0)

= a^0 : by simp [nat.mul_zero]

... = 1 : by simp

... = (a^m)^0 : by simp },

{ calc a^(m * succ n)

= a^(m * n + m) : by simp [nat.mul_succ]

... = a^(m * n) * a^m : by simp [pow_add]

... = (a^m)^n * a^m : by simp [HI]

... = (a^m)^succ n : by simp [pow_succ'] },

end

-- 4ª demostración

-- ===============

example : a^(m * n) = (a^m)^n :=

begin

induction n with n HI,

{ by simp [nat.mul_zero] },

{ by simp [nat.mul_succ,

pow_add,

HI,

pow_succ'] },

end

-- 5ª demostración

-- ===============

example : a^(m * n) = (a^m)^n :=

begin

induction n with n HI,

{ rw nat.mul_zero,

rw pow_zero,

rw pow_zero, },

{ rw nat.mul_succ,

rw pow_add,

rw HI,

rw pow_succ', }

end

-- 6ª demostración

-- ===============

example : a^(m * n) = (a^m)^n :=

begin

induction n with n HI,

{ rw [nat.mul_zero, pow_zero, pow_zero] },

{ rw [nat.mul_succ, pow_add, HI, pow_succ'] }

end

-- 7ª demostración

-- ===============

example : a^(m * n) = (a^m)^n :=

pow_mul a m n

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

(* Potencias_de_potencias_en_monoides.thy
theory Potencias_de_potencias_en_monoides
imports Main
begin

context monoid_mult
begin

(* 1ª demostración *)

lemma  "a^(m * n) = (a^m)^n"
proof (induct n)
  have "a ^ (m * 0) = a ^ 0"
    by (simp only: mult_0_right)
  also have "… = 1"
    by (simp only: power_0)
  also have "… = (a ^ m) ^ 0"
    by (simp only: power_0)
  finally show "a ^ (m * 0) = (a ^ m) ^ 0"
    by this
next
  fix n
  assume HI : "a ^ (m * n) = (a ^ m) ^ n"
  have "a ^ (m * Suc n) = a ^ (m + m * n)"
    by (simp only: mult_Suc_right)
  also have "… = a ^ m * a ^ (m * n)"
    by (simp only: power_add)
  also have "… = a ^ m * (a ^ m) ^ n"
    by (simp only: HI)
  also have "… = (a ^ m) ^ Suc n"
    by (simp only: power_Suc)
  finally show "a ^ (m * Suc n) = (a ^ m) ^ Suc n"
    by this
qed

(* 2ª demostración *)

lemma  "a^(m * n) = (a^m)^n"
proof (induct n)
  have "a ^ (m * 0) = a ^ 0"               by simp
  also have "… = 1"                        by simp
  also have "… = (a ^ m) ^ 0"              by simp
  finally show "a ^ (m * 0) = (a ^ m) ^ 0" .
next
  fix n
  assume HI : "a ^ (m * n) = (a ^ m) ^ n"
  have "a ^ (m * Suc n) = a ^ (m + m * n)" by simp
  also have "… = a ^ m * a ^ (m * n)"      by (simp add: power_add)
  also have "… = a ^ m * (a ^ m) ^ n"      using HI by simp
  also have "… = (a ^ m) ^ Suc n"          by simp
  finally show "a ^ (m * Suc n) =
                (a ^ m) ^ Suc n"           .
qed

(* 3ª demostración *)

lemma  "a^(m * n) = (a^m)^n"
proof (induct n)
  case 0
  then show ?case by simp
next
  case (Suc n)
  then show ?case by (simp add: power_add)
qed

(* 4ª demostración *)

lemma  "a^(m * n) = (a^m)^n"
  by (induct n) (simp_all add: power_add)

(* 5ª demostración *)

lemma "a^(m * n) = (a^m)^n"
  by (simp only: power_mult)

end

end

(* Potencias_de_potencias_en_monoides.thy

theory Potencias_de_potencias_en_monoides

imports Main

begin

context monoid_mult

begin

(* 1ª demostración *)

lemma "a^(m * n) = (a^m)^n"

proof (induct n)

have "a ^ (m * 0) = a ^ 0"

by (simp only: mult_0_right)

also have "… = 1"

by (simp only: power_0)

also have "… = (a ^ m) ^ 0"

by (simp only: power_0)

finally show "a ^ (m * 0) = (a ^ m) ^ 0"

by this

fix n

assume HI : "a ^ (m * n) = (a ^ m) ^ n"

have "a ^ (m * Suc n) = a ^ (m + m * n)"

by (simp only: mult_Suc_right)

also have "… = a ^ m * a ^ (m * n)"

by (simp only: power_add)

also have "… = a ^ m * (a ^ m) ^ n"

by (simp only: HI)

also have "… = (a ^ m) ^ Suc n"

by (simp only: power_Suc)

finally show "a ^ (m * Suc n) = (a ^ m) ^ Suc n"

by this

qed

(* 2ª demostración *)

lemma "a^(m * n) = (a^m)^n"

proof (induct n)

have "a ^ (m * 0) = a ^ 0" by simp

also have "… = 1" by simp

also have "… = (a ^ m) ^ 0" by simp

finally show "a ^ (m * 0) = (a ^ m) ^ 0" .

fix n

assume HI : "a ^ (m * n) = (a ^ m) ^ n"

have "a ^ (m * Suc n) = a ^ (m + m * n)" by simp

also have "… = a ^ m * a ^ (m * n)" by (simp add: power_add)

also have "… = a ^ m * (a ^ m) ^ n" using HI by simp

also have "… = (a ^ m) ^ Suc n" by simp

finally show "a ^ (m * Suc n) =

(a ^ m) ^ Suc n" .

qed

(* 3ª demostración *)

lemma "a^(m * n) = (a^m)^n"

proof (induct n)

case 0

then show ?case by simp

case (Suc n)

then show ?case by (simp add: power_add)

qed

(* 4ª demostración *)

lemma "a^(m * n) = (a^m)^n"

by (induct n) (simp_all add: power_add)

(* 5ª demostración *)

lemma "a^(m * n) = (a^m)^n"

by (simp only: power_mult)

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Propiedad cancelativa en grupos

PorJosé A. Alonso 8 julio 20214 julio 2021

Sea G un grupo y a,b,c ∈ G. Demostrar que si a * b = a* c, entonces b = c.

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

import algebra.group.basic

universe  u
variables {G : Type u} [group G]
variables {a b c : G}

example
  (h: a * b = a  * c)
  : b = c :=
sorry

import algebra.group.basic

universe u

variables {G : Type u} [group G]

variables {a b c : G}

example

(h: a * b = a * c)

: b = c :=

sorry

[expand title=»Soluciones con Lean»]

import algebra.group.basic

universe  u
variables {G : Type u} [group G]
variables {a b c : G}

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

example
  (h: a * b = a  * c)
  : b = c :=
calc b = 1 * b         : (one_mul b).symm
   ... = (a⁻¹ * a) * b : congr_arg (* b) (inv_mul_self a).symm
   ... = a⁻¹ * (a * b) : mul_assoc a⁻¹ a b
   ... = a⁻¹ * (a * c) : congr_arg ((*) a⁻¹) h
   ... = (a⁻¹ * a) * c : (mul_assoc a⁻¹ a c).symm
   ... = 1 * c         : congr_arg (* c) (inv_mul_self a)
   ... = c             : one_mul c

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

example
  (h: a * b = a  * c)
  : b = c :=
calc b = 1 * b         : by rw one_mul
   ... = (a⁻¹ * a) * b : by rw inv_mul_self
   ... = a⁻¹ * (a * b) : by rw mul_assoc
   ... = a⁻¹ * (a * c) : by rw h
   ... = (a⁻¹ * a) * c : by rw mul_assoc
   ... = 1 * c         : by rw inv_mul_self
   ... = c             : by rw one_mul

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

example
  (h: a * b = a  * c)
  : b = c :=
calc b = 1 * b         : by simp
   ... = (a⁻¹ * a) * b : by simp
   ... = a⁻¹ * (a * b) : by simp
   ... = a⁻¹ * (a * c) : by simp [h]
   ... = (a⁻¹ * a) * c : by simp
   ... = 1 * c         : by simp
   ... = c             : by simp

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

example
  (h: a * b = a  * c)
  : b = c :=
calc b = a⁻¹ * (a * b) : by simp
   ... = a⁻¹ * (a * c) : by simp [h]
   ... = c             : by simp

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

example
  (h: a * b = a  * c)
  : b = c :=
begin
  have h1 : a⁻¹ * (a * b) = a⁻¹ * (a  * c),
    { by finish [h] },
  have h2 : (a⁻¹ * a) * b = (a⁻¹ * a)  * c,
    { by finish },
  have h3 : 1 * b = 1  * c,
    { by finish },
  have h3 : b = c,
    { by finish },
  exact h3,
end

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

example
  (h: a * b = a  * c)
  : b = c :=
begin
  have : a⁻¹ * (a * b) = a⁻¹ * (a  * c),
    { by finish [h] },
  have h2 : (a⁻¹ * a) * b = (a⁻¹ * a)  * c,
    { by finish },
  have h3 : 1 * b = 1  * c,
    { by finish },
  have h3 : b = c,
    { by finish },
  exact h3,
end

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

example
  (h: a * b = a  * c)
  : b = c :=
begin
  have h1 : a⁻¹ * (a * b) = a⁻¹ * (a  * c),
    { congr, exact h, },
  have h2 : (a⁻¹ * a) * b = (a⁻¹ * a)  * c,
    { simp only [h1, mul_assoc], },
  have h3 : 1 * b = 1  * c,
    { simp only [h2, (inv_mul_self a).symm], },
  rw one_mul at h3,
  rw one_mul at h3,
  exact h3,
end

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

example
  (h: a * b = a  * c)
  : b = c :=
mul_left_cancel h

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

example
  (h: a * b = a  * c)
  : b = c :=
by finish

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

123

124

125

126

127

import algebra.group.basic

universe u

variables {G : Type u} [group G]

variables {a b c : G}

-- 1ª demostración

-- ===============

example

(h: a * b = a * c)

: b = c :=

calc b = 1 * b : (one_mul b).symm

... = (a⁻¹ * a) * b : congr_arg (* b) (inv_mul_self a).symm

... = a⁻¹ * (a * b) : mul_assoc a⁻¹ a b

... = a⁻¹ * (a * c) : congr_arg ((*) a⁻¹) h

... = (a⁻¹ * a) * c : (mul_assoc a⁻¹ a c).symm

... = 1 * c : congr_arg (* c) (inv_mul_self a)

... = c : one_mul c

-- 2ª demostración

-- ===============

example

(h: a * b = a * c)

: b = c :=

calc b = 1 * b : by rw one_mul

... = (a⁻¹ * a) * b : by rw inv_mul_self

... = a⁻¹ * (a * b) : by rw mul_assoc

... = a⁻¹ * (a * c) : by rw h

... = (a⁻¹ * a) * c : by rw mul_assoc

... = 1 * c : by rw inv_mul_self

... = c : by rw one_mul

-- 3ª demostración

-- ===============

example

(h: a * b = a * c)

: b = c :=

calc b = 1 * b : by simp

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

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

... = a⁻¹ * (a * c) : by simp [h]

... = (a⁻¹ * a) * c : by simp

... = 1 * c : by simp

... = c : by simp

-- 4ª demostración

-- ===============

example

(h: a * b = a * c)

: b = c :=

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

... = a⁻¹ * (a * c) : by simp [h]

... = c : by simp

-- 4ª demostración

-- ===============

example

(h: a * b = a * c)

: b = c :=

begin

have h1 : a⁻¹ * (a * b) = a⁻¹ * (a * c),

{ by finish [h] },

have h2 : (a⁻¹ * a) * b = (a⁻¹ * a) * c,

{ by finish },

have h3 : 1 * b = 1 * c,

{ by finish },

have h3 : b = c,

{ by finish },

exact h3,

end

-- 4ª demostración

-- ===============

example

(h: a * b = a * c)

: b = c :=

begin

have : a⁻¹ * (a * b) = a⁻¹ * (a * c),

{ by finish [h] },

have h2 : (a⁻¹ * a) * b = (a⁻¹ * a) * c,

{ by finish },

have h3 : 1 * b = 1 * c,

{ by finish },

have h3 : b = c,

{ by finish },

exact h3,

end

-- 4ª demostración

-- ===============

example

(h: a * b = a * c)

: b = c :=

begin

have h1 : a⁻¹ * (a * b) = a⁻¹ * (a * c),

{ congr, exact h, },

have h2 : (a⁻¹ * a) * b = (a⁻¹ * a) * c,

{ simp only [h1, mul_assoc], },

have h3 : 1 * b = 1 * c,

{ simp only [h2, (inv_mul_self a).symm], },

rw one_mul at h3,

exact h3,

end

-- 5ª demostración

-- ===============

example

(h: a * b = a * c)

: b = c :=

mul_left_cancel h

-- 6ª demostración

-- ===============

example

(h: a * b = a * c)

: b = c :=

by finish

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory Propiedad_cancelativa_en_grupos
imports Main
begin

context group
begin

(* 1ª demostración *)

lemma
  assumes "a * b = a * c"
  shows   "b = c"
proof -
  have "b = 1 * b"                    by (simp only: left_neutral)
  also have "… = (inverse a * a) * b" by (simp only: left_inverse)
  also have "… = inverse a * (a * b)" by (simp only: assoc)
  also have "… = inverse a * (a * c)" by (simp only: ‹a * b = a * c›)
  also have "… = (inverse a * a) * c" by (simp only: assoc)
  also have "… = 1 * c"               by (simp only: left_inverse)
  also have "… = c"                   by (simp only: left_neutral)
  finally show "b = c"                by this
qed

(* 2ª demostración *)

lemma
  assumes "a * b = a * c"
  shows   "b = c"
proof -
  have "b = 1 * b"                    by simp
  also have "… = (inverse a * a) * b" by simp
  also have "… = inverse a * (a * b)" by (simp only: assoc)
  also have "… = inverse a * (a * c)" using ‹a * b = a * c› by simp
  also have "… = (inverse a * a) * c" by (simp only: assoc)
  also have "… = 1 * c"               by simp
  finally show "b = c"                by simp
qed

(* 3ª demostración *)

lemma
  assumes "a * b = a * c"
  shows   "b = c"
proof -
  have "b = (inverse a * a) * b"      by simp
  also have "… = inverse a * (a * b)" by (simp only: assoc)
  also have "… = inverse a * (a * c)" using ‹a * b = a * c› by simp
  also have "… = (inverse a * a) * c" by (simp only: assoc)
  finally show "b = c"                by simp
qed

(* 4ª demostración *)

lemma
  assumes "a * b = a * c"
  shows   "b = c"
proof -
  have "inverse a * (a * b) = inverse a * (a * c)"
    by (simp only: ‹a * b = a * c›)
  then have "(inverse a * a) * b = (inverse a * a) * c"
    by (simp only: assoc)
  then have "1 * b = 1 * c"
    by (simp only: left_inverse)
  then show "b = c"
    by (simp only: left_neutral)
qed

(* 5ª demostración *)

lemma
  assumes "a * b = a * c"
  shows   "b = c"
proof -
  have "inverse a * (a * b) = inverse a * (a * c)"
    by (simp only: ‹a * b = a * c›)
  then have "(inverse a * a) * b = (inverse a * a) * c"
    by (simp only: assoc)
  then have "1 * b = 1 * c"
    by (simp only: left_inverse)
  then show "b = c"
    by (simp only: left_neutral)
qed

(* 6ª demostración *)

lemma
  assumes "a * b = a * c"
  shows   "b = c"
proof -
  have "inverse a * (a * b) = inverse a * (a * c)"
    using ‹a * b = a * c› by simp
  then have "(inverse a * a) * b = (inverse a * a) * c"
    by (simp only: assoc)
  then have "1 * b = 1 * c"
    by simp
  then show "b = c"
    by simp
qed

(* 7ª demostración *)

lemma
  assumes "a * b = a * c"
  shows   "b = c"
  using assms
  by (simp only: left_cancel)

end

end

100

101

102

103

104

105

106

107

108

109

110

theory Propiedad_cancelativa_en_grupos

imports Main

begin

context group

begin

(* 1ª demostración *)

lemma

assumes "a * b = a * c"

shows "b = c"

proof -

have "b = 1 * b" by (simp only: left_neutral)

also have "… = (inverse a * a) * b" by (simp only: left_inverse)

also have "… = inverse a * (a * b)" by (simp only: assoc)

also have "… = inverse a * (a * c)" by (simp only: ‹a * b = a * c›)

also have "… = (inverse a * a) * c" by (simp only: assoc)

also have "… = 1 * c" by (simp only: left_inverse)

also have "… = c" by (simp only: left_neutral)

finally show "b = c" by this

qed

(* 2ª demostración *)

lemma

assumes "a * b = a * c"

shows "b = c"

proof -

have "b = 1 * b" by simp

also have "… = (inverse a * a) * b" by simp

also have "… = inverse a * (a * b)" by (simp only: assoc)

also have "… = inverse a * (a * c)" using ‹a * b = a * c› by simp

also have "… = (inverse a * a) * c" by (simp only: assoc)

also have "… = 1 * c" by simp

finally show "b = c" by simp

qed

(* 3ª demostración *)

lemma

assumes "a * b = a * c"

shows "b = c"

proof -

have "b = (inverse a * a) * b" by simp

also have "… = inverse a * (a * b)" by (simp only: assoc)

also have "… = inverse a * (a * c)" using ‹a * b = a * c› by simp

also have "… = (inverse a * a) * c" by (simp only: assoc)

finally show "b = c" by simp

qed

(* 4ª demostración *)

lemma

assumes "a * b = a * c"

shows "b = c"

proof -

have "inverse a * (a * b) = inverse a * (a * c)"

by (simp only: ‹a * b = a * c›)

then have "(inverse a * a) * b = (inverse a * a) * c"

by (simp only: assoc)

then have "1 * b = 1 * c"

by (simp only: left_inverse)

then show "b = c"

by (simp only: left_neutral)

qed

(* 5ª demostración *)

lemma

assumes "a * b = a * c"

shows "b = c"

proof -

have "inverse a * (a * b) = inverse a * (a * c)"

by (simp only: ‹a * b = a * c›)

then have "(inverse a * a) * b = (inverse a * a) * c"

by (simp only: assoc)

then have "1 * b = 1 * c"

by (simp only: left_inverse)

then show "b = c"

by (simp only: left_neutral)

qed

(* 6ª demostración *)

lemma

assumes "a * b = a * c"

shows "b = c"

proof -

have "inverse a * (a * b) = inverse a * (a * c)"

using ‹a * b = a * c› by simp

then have "(inverse a * a) * b = (inverse a * a) * c"

by (simp only: assoc)

then have "1 * b = 1 * c"

by simp

then show "b = c"

by simp

qed

(* 7ª demostración *)

lemma

assumes "a * b = a * c"

shows "b = c"

using assms

by (simp only: left_cancel)

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Inverso del inverso en grupos

PorJosé A. Alonso 7 julio 20214 julio 2021

Sea G un grupo y a ∈ G. Demostrar que

    (a⁻¹)⁻¹ = a

1	(a⁻¹)⁻¹ = a

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

import algebra.group.basic

universe  u
variables {G : Type u} [group G]
variables {a b : G}

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

import algebra.group.basic

universe u

variables {G : Type u} [group G]

variables {a b : G}

example : (a⁻¹)⁻¹ = a :=

sorry

[expand title=»Soluciones con Lean»]

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 inv_eq_of_mul_eq_one,
  exact mul_left_inv a,
end

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

example : (a⁻¹)⁻¹ = a :=
inv_eq_of_mul_eq_one (mul_left_inv a)

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

example : (a⁻¹)⁻¹ = a:=
inv_inv a

-- 7ª demostración
-- ===============

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

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

exact mul_left_inv a,

end

-- 5ª demostración

-- ===============

example : (a⁻¹)⁻¹ = a :=

inv_eq_of_mul_eq_one (mul_left_inv a)

-- 6ª demostración

-- ===============

example : (a⁻¹)⁻¹ = a:=

inv_inv a

-- 7ª demostración

-- ===============

example : (a⁻¹)⁻¹ = a:=

by simp

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory Inverso_del_inverso_en_grupos
imports Main
begin

context group
begin

(* 1ª demostración *)

lemma "inverse (inverse a) = a"
proof -
  have "inverse (inverse a) =
        (inverse (inverse a)) * 1"
    by (simp only: right_neutral)
  also have "… = inverse (inverse a) * (inverse a * a)"
    by (simp only: left_inverse)
  also have "… = (inverse (inverse a) * inverse a) * a"
    by (simp only: assoc)
  also have "… = 1 * a"
    by (simp only: left_inverse)
  also have "… = a"
    by (simp only: left_neutral)
  finally show "inverse (inverse a) = a"
    by this
qed

(* 2ª demostración *)

lemma "inverse (inverse a) = a"
proof -
  have "inverse (inverse a) =
        (inverse (inverse a)) * 1"                      by simp
  also have "… = inverse (inverse a) * (inverse a * a)" by simp
  also have "… = (inverse (inverse a) * inverse a) * a" by simp
  also have "… = 1 * a"                                 by simp
  finally show "inverse (inverse a) = a"                by simp
qed

(* 3ª demostración *)

lemma "inverse (inverse a) = a"
proof (rule inverse_unique)
  show "inverse a * a = 1"
    by (simp only: left_inverse)
qed

(* 4ª demostración *)

lemma "inverse (inverse a) = a"
proof (rule inverse_unique)
  show "inverse a * a = 1" by simp
qed

(* 5ª demostración *)

lemma "inverse (inverse a) = a"
  by (rule inverse_unique) simp

(* 6ª demostración *)

lemma "inverse (inverse a) = a"
  by (simp only: inverse_inverse)

(* 7ª demostración *)

lemma "inverse (inverse a) = a"
  by simp

end

end

theory Inverso_del_inverso_en_grupos

imports Main

begin

context group

begin

(* 1ª demostración *)

lemma "inverse (inverse a) = a"

proof -

have "inverse (inverse a) =

(inverse (inverse a)) * 1"

by (simp only: right_neutral)

also have "… = inverse (inverse a) * (inverse a * a)"

by (simp only: left_inverse)

also have "… = (inverse (inverse a) * inverse a) * a"

by (simp only: assoc)

also have "… = 1 * a"

by (simp only: left_inverse)

also have "… = a"

by (simp only: left_neutral)

finally show "inverse (inverse a) = a"

by this

qed

(* 2ª demostración *)

lemma "inverse (inverse a) = a"

proof -

have "inverse (inverse a) =

(inverse (inverse a)) * 1" by simp

also have "… = inverse (inverse a) * (inverse a * a)" by simp

also have "… = (inverse (inverse a) * inverse a) * a" by simp

also have "… = 1 * a" by simp

finally show "inverse (inverse a) = a" by simp

qed

(* 3ª demostración *)

lemma "inverse (inverse a) = a"

proof (rule inverse_unique)

show "inverse a * a = 1"

by (simp only: left_inverse)

qed

(* 4ª demostración *)

lemma "inverse (inverse a) = a"

proof (rule inverse_unique)

show "inverse a * a = 1" by simp

qed

(* 5ª demostración *)

lemma "inverse (inverse a) = a"

by (rule inverse_unique) simp

(* 6ª demostración *)

lemma "inverse (inverse a) = a"

by (simp only: inverse_inverse)

(* 7ª demostración *)

lemma "inverse (inverse a) = a"

by simp

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Referencia

Propiedad 3.20 del libro Abstract algebra: Theory and applications de Thomas W. Judson.

Inverso del producto

PorJosé A. Alonso 6 julio 20214 julio 2021

Sea G un grupo y a, b ∈ G. Entonces,

   (a * b)⁻¹ = b⁻¹ * a⁻¹

1	(a * b)⁻¹ = b⁻¹ * a⁻¹

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

import algebra.group.basic

universe  u
variables {G : Type u} [group G]
variables {a b : G}

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

import algebra.group.basic

universe u

variables {G : Type u} [group G]

variables {a b : G}

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

begin

sorry

[expand title=»Soluciones con Lean»]

import algebra.group.basic

universe  u
variables {G : Type u} [group G]
variables {a b : G}

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

example : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
begin
  apply inv_eq_of_mul_eq_one,
  calc a * b * (b⁻¹ * a⁻¹)
       = ((a * b) * b⁻¹) * a⁻¹ : (mul_assoc _ _ _).symm
   ... = (a * (b * b⁻¹)) * a⁻¹ : congr_arg (* a⁻¹) (mul_assoc a _ _)
   ... = (a * 1) * a⁻¹         : congr_arg2 _ (congr_arg _ (mul_inv_self b)) rfl
   ... = a * a⁻¹               : congr_arg (* a⁻¹) (mul_one a)
   ... = 1                     : mul_inv_self a
end

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

example : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
begin
  apply inv_eq_of_mul_eq_one,
  calc a * b * (b⁻¹ * a⁻¹)
       = ((a * b) * b⁻¹) * a⁻¹ : by simp only [mul_assoc]
   ... = (a * (b * b⁻¹)) * a⁻¹ : by simp only [mul_assoc]
   ... = (a * 1) * a⁻¹         : by simp only [mul_inv_self]
   ... = a * a⁻¹               : by simp only [mul_one]
   ... = 1                     : by simp only [mul_inv_self]
end

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

example : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
begin
  apply inv_eq_of_mul_eq_one,
  calc a * b * (b⁻¹ * a⁻¹)
       = ((a * b) * b⁻¹) * a⁻¹ : by simp [mul_assoc]
   ... = (a * (b * b⁻¹)) * a⁻¹ : by simp
   ... = (a * 1) * a⁻¹         : by simp
   ... = a * a⁻¹               : by simp
   ... = 1                     : by simp,
end

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

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

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

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

import algebra.group.basic

universe u

variables {G : Type u} [group G]

variables {a b : G}

-- 1ª demostración

-- ===============

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

begin

apply inv_eq_of_mul_eq_one,

calc a * b * (b⁻¹ * a⁻¹)

= ((a * b) * b⁻¹) * a⁻¹ : (mul_assoc _ _ _).symm

... = (a * (b * b⁻¹)) * a⁻¹ : congr_arg (* a⁻¹) (mul_assoc a _ _)

... = (a * 1) * a⁻¹ : congr_arg2 _ (congr_arg _ (mul_inv_self b)) rfl

... = a * a⁻¹ : congr_arg (* a⁻¹) (mul_one a)

... = 1 : mul_inv_self a

end

-- 2ª demostración

-- ===============

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

begin

apply inv_eq_of_mul_eq_one,

calc a * b * (b⁻¹ * a⁻¹)

= ((a * b) * b⁻¹) * a⁻¹ : by simp only [mul_assoc]

... = (a * (b * b⁻¹)) * a⁻¹ : by simp only [mul_assoc]

... = (a * 1) * a⁻¹ : by simp only [mul_inv_self]

... = a * a⁻¹ : by simp only [mul_one]

... = 1 : by simp only [mul_inv_self]

end

-- 3ª demostración

-- ===============

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

begin

apply inv_eq_of_mul_eq_one,

calc a * b * (b⁻¹ * a⁻¹)

= ((a * b) * b⁻¹) * a⁻¹ : by simp [mul_assoc]

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

... = (a * 1) * a⁻¹ : by simp

... = a * a⁻¹ : by simp

... = 1 : by simp,

end

-- 4ª demostración

-- ===============

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

mul_inv_rev a b

-- 5ª demostración

-- ===============

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

by simp

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones 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)

(* ?ª demostración *)

end

end

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)

(* ?ª demostración *)

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Referencia

Propiedad 3.19 del libro Abstract algebra: Theory and applications de Thomas W. Judson.

Unicidad de los inversos en los grupos

PorJosé A. Alonso 5 julio 20214 julio 2021

Demostrar que si a es un elemento de un grupo G, entonces a tiene un único inverso; es decir, si b es un elemento de G tal que a * b = 1, entonces a⁻¹ = b.

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

import algebra.group.basic

universe  u
variables {G : Type u} [group G]
variables {a b : G}

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

import algebra.group.basic

universe u

variables {G : Type u} [group G]

variables {a b : G}

example

(h : a * b = 1)

: a⁻¹ = b :=

sorry

[expand title=»Soluciones con Lean»]

import algebra.group.basic

universe  u
variables {G : Type u} [group G]
variables {a b : G}

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

example
  (h : a * b = 1)
  : a⁻¹ = b :=
calc a⁻¹ = a⁻¹ * 1       : (mul_one a⁻¹).symm
     ... = a⁻¹ * (a * b) : congr_arg ((*) a⁻¹) h.symm
     ... = (a⁻¹ * a) * b : (mul_assoc a⁻¹ a b).symm
     ... = 1 * b         : congr_arg (* b) (inv_mul_self a)
     ... = b             : one_mul b

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

example
  (h : a * b = 1)
  : a⁻¹ = b :=
calc a⁻¹ = a⁻¹ * 1       : by simp only [mul_one]
     ... = a⁻¹ * (a * b) : by simp only [h]
     ... = (a⁻¹ * a) * b : by simp only [mul_assoc]
     ... = 1 * b         : by simp only [inv_mul_self]
     ... = b             : by simp only [one_mul]

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

example
  (h : a * b = 1)
  : a⁻¹ = b :=
calc a⁻¹ = a⁻¹ * 1       : by simp
     ... = a⁻¹ * (a * b) : by simp [h]
     ... = (a⁻¹ * a) * b : by simp
     ... = 1 * b         : by simp
     ... = b             : by simp

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

example
  (h : a * b = 1)
  : a⁻¹ = b :=
calc a⁻¹ = a⁻¹ * (a * b) : by simp [h]
     ... = b             : by simp

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

example
  (h : b * a = 1)
  : b = a⁻¹ :=
eq_inv_of_mul_eq_one h

import algebra.group.basic

universe u

variables {G : Type u} [group G]

variables {a b : G}

-- 1ª demostración

-- ===============

example

(h : a * b = 1)

: a⁻¹ = b :=

calc a⁻¹ = a⁻¹ * 1 : (mul_one a⁻¹).symm

... = a⁻¹ * (a * b) : congr_arg ((*) a⁻¹) h.symm

... = (a⁻¹ * a) * b : (mul_assoc a⁻¹ a b).symm

... = 1 * b : congr_arg (* b) (inv_mul_self a)

... = b : one_mul b

-- 2ª demostración

-- ===============

example

(h : a * b = 1)

: a⁻¹ = b :=

calc a⁻¹ = a⁻¹ * 1 : by simp only [mul_one]

... = a⁻¹ * (a * b) : by simp only [h]

... = (a⁻¹ * a) * b : by simp only [mul_assoc]

... = 1 * b : by simp only [inv_mul_self]

... = b : by simp only [one_mul]

-- 3ª demostración

-- ===============

example

(h : a * b = 1)

: a⁻¹ = b :=

calc a⁻¹ = a⁻¹ * 1 : by simp

... = a⁻¹ * (a * b) : by simp [h]

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

... = 1 * b : by simp

... = b : by simp

-- 4ª demostración

-- ===============

example

(h : a * b = 1)

: a⁻¹ = b :=

calc a⁻¹ = a⁻¹ * (a * b) : by simp [h]

... = b : by simp

-- 5ª demostración

-- ===============

example

(h : b * a = 1)

: b = a⁻¹ :=

eq_inv_of_mul_eq_one h

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory Unicidad_de_los_inversos_en_los_grupos
imports Main
begin

context group
begin

(* 1ª demostración *)

lemma
  assumes "a * b = 1"
  shows "inverse a = b"
proof -
  have "inverse a = inverse a * 1"    by (simp only: right_neutral)
  also have "… = inverse a * (a * b)" by (simp only: assms(1))
  also have "… = (inverse a * a) * b" by (simp only: assoc [symmetric])
  also have "… = 1 * b"               by (simp only: left_inverse)
  also have "… = b"                   by (simp only: left_neutral)
  finally show "inverse a = b"        by this
qed

(* 2ª demostración *)

lemma
  assumes "a * b = 1"
  shows "inverse a = b"
proof -
  have "inverse a = inverse a * 1"    by simp
  also have "… = inverse a * (a * b)" using assms by simp
  also have "… = (inverse a * a) * b" by (simp add: assoc [symmetric])
  also have "… = 1 * b"               by simp
  also have "… = b"                   by simp
  finally show "inverse a = b"        .
qed

(* 3ª demostración *)

lemma
  assumes "a * b = 1"
  shows "inverse a = b"
proof -
  from assms have "inverse a * (a * b) = inverse a"
    by simp
  then show "inverse a = b"
    by (simp add: assoc [symmetric])
qed

(* 4ª demostración *)

lemma
  assumes "a * b = 1"
  shows "inverse a = b"
  using assms
  by (simp only: inverse_unique)

end

end

theory Unicidad_de_los_inversos_en_los_grupos

imports Main

begin

context group

begin

(* 1ª demostración *)

lemma

assumes "a * b = 1"

shows "inverse a = b"

proof -

have "inverse a = inverse a * 1" by (simp only: right_neutral)

also have "… = inverse a * (a * b)" by (simp only: assms(1))

also have "… = (inverse a * a) * b" by (simp only: assoc [symmetric])

also have "… = 1 * b" by (simp only: left_inverse)

also have "… = b" by (simp only: left_neutral)

finally show "inverse a = b" by this

qed

(* 2ª demostración *)

lemma

assumes "a * b = 1"

shows "inverse a = b"

proof -

have "inverse a = inverse a * 1" by simp

also have "… = inverse a * (a * b)" using assms by simp

also have "… = (inverse a * a) * b" by (simp add: assoc [symmetric])

also have "… = 1 * b" by simp

also have "… = b" by simp

finally show "inverse a = b" .

qed

(* 3ª demostración *)

lemma

assumes "a * b = 1"

shows "inverse a = b"

proof -

from assms have "inverse a * (a * b) = inverse a"

by simp

then show "inverse a = b"

by (simp add: assoc [symmetric])

qed

(* 4ª demostración *)

lemma

assumes "a * b = 1"

shows "inverse a = b"

using assms

by (simp only: inverse_unique)

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Referencia

Propiedad 3.18 del libro Abstract algebra: Theory and applications de Thomas W. Judson.

Unicidad del elemento neutro en los grupos

PorJosé A. Alonso 4 julio 20214 julio 2021

Demostrar que un grupo sólo posee un elemento neutro.

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

import algebra.group.basic

universe  u
variables {G : Type u} [group G]

example
  (e : G)
  (h : ∀ x, x * e = x)
  : e = 1 :=
sorry

import algebra.group.basic

universe u

variables {G : Type u} [group G]

example

(e : G)

(h : ∀ x, x * e = x)

: e = 1 :=

sorry

[expand title=»Soluciones con Lean»]

import algebra.group.basic

universe  u
variables {G : Type u} [group G]

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

example
  (e : G)
  (h : ∀ x, x * e = x)
  : e = 1 :=
calc e = 1 * e : (one_mul e).symm
   ... = 1     : h 1

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

example
  (e : G)
  (h : ∀ x, x * e = x)
  : e = 1 :=
by finish

import algebra.group.basic

universe u

variables {G : Type u} [group G]

-- 1ª demostración

-- ===============

example

(e : G)

(h : ∀ x, x * e = x)

: e = 1 :=

calc e = 1 * e : (one_mul e).symm

... = 1 : h 1

-- 2ª demostración

-- ===============

example

(e : G)

(h : ∀ x, x * e = x)

: e = 1 :=

by finish

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory Unicidad_del_elemento_neutro_en_los_grupos
imports Main
begin

context group
begin

(* 1ª demostración *)

lemma
  assumes "∀ x. x * e = x"
  shows   "e = 1"
proof -
  have "e = 1 * e"     by (simp only: left_neutral)
  also have "… = 1"    using assms by (rule allE)
  finally show "e = 1" by this
qed

(* 2ª demostración *)

lemma
  assumes "∀ x. x * e = x"
  shows   "e = 1"
proof -
  have "e = 1 * e"     by simp
  also have "… = 1"    using assms by simp
  finally show "e = 1" .
qed

(* 3ª demostración *)

lemma
  assumes "∀ x. x * e = x"
  shows   "e = 1"
  using assms
  by (metis left_neutral)

end

end

theory Unicidad_del_elemento_neutro_en_los_grupos

imports Main

begin

context group

begin

(* 1ª demostración *)

lemma

assumes "∀ x. x * e = x"

shows "e = 1"

proof -

have "e = 1 * e" by (simp only: left_neutral)

also have "… = 1" using assms by (rule allE)

finally show "e = 1" by this

qed

(* 2ª demostración *)

lemma

assumes "∀ x. x * e = x"

shows "e = 1"

proof -

have "e = 1 * e" by simp

also have "… = 1" using assms by simp

finally show "e = 1" .

qed

(* 3ª demostración *)

lemma

assumes "∀ x. x * e = x"

shows "e = 1"

using assms

by (metis left_neutral)

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Referencia

Propiedad 3.17 del libro Abstract algebra: Theory and applications de Thomas W. Judson.

Caracterización de producto igual al primer factor

PorJosé A. Alonso 3 julio 202124 junio 2021

Un monoide cancelativo por la izquierda es un monoide M que cumple la propiedad cancelativa por la izquierda; es decir, para todo a, b ∈ M

   a * b = a * c ↔ b = c.

1	a * b = a * c ↔ b = c.

En Lean la clase de los monoides cancelativos por la izquierda es left_cancel_monoid y la propiedad cancelativa por la izquierda es

   mul_left_cancel_iff : a * b = a * c ↔ b = c

1	mul_left_cancel_iff : a * b = a * c ↔ b = c

Demostrar que si M es un monoide cancelativo por la izquierda y a, b ∈ M, entonces

   a * b = a ↔ b = 1

1	a * b = a ↔ b = 1

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

import algebra.group.basic

universe  u
variables {M : Type u} [left_cancel_monoid M]
variables {a b : M}

example : a * b = a ↔ b = 1 :=
sorry

import algebra.group.basic

universe u

variables {M : Type u} [left_cancel_monoid M]

variables {a b : M}

example : a * b = a ↔ b = 1 :=

sorry

[expand title=»Soluciones con Lean»]

import algebra.group.basic

universe  u
variables {M : Type u} [left_cancel_monoid M]
variables {a b : M}

-- ?ª demostración
-- ===============

example : a * b = a ↔ b = 1 :=
begin
  split,
  { intro h,
    rw ← @mul_left_cancel_iff _ _ a b 1,
    rw mul_one,
    exact h, },
  { intro h,
    rw h,
    exact mul_one a, },
end

-- ?ª demostración
-- ===============

example : a * b = a ↔ b = 1 :=
calc a * b = a ↔ a * b = a * 1 : by rw mul_one
           ... ↔ b = 1         : mul_left_cancel_iff

-- ?ª demostración
-- ===============

example : a * b = a ↔ b = 1 :=
mul_right_eq_self

-- ?ª demostración
-- ===============

example : a * b = a ↔ b = 1 :=
by finish

import algebra.group.basic

universe u

variables {M : Type u} [left_cancel_monoid M]

variables {a b : M}

-- ?ª demostración

-- ===============

example : a * b = a ↔ b = 1 :=

begin

split,

{ intro h,

rw ← @mul_left_cancel_iff _ _ a b 1,

rw mul_one,

exact h, },

{ intro h,

rw h,

exact mul_one a, },

end

-- ?ª demostración

-- ===============

example : a * b = a ↔ b = 1 :=

calc a * b = a ↔ a * b = a * 1 : by rw mul_one

... ↔ b = 1 : mul_left_cancel_iff

-- ?ª demostración

-- ===============

example : a * b = a ↔ b = 1 :=

mul_right_eq_self

-- ?ª demostración

-- ===============

example : a * b = a ↔ b = 1 :=

by finish

Se puede interactuar con la prueba anterior en esta sesión con Lean,

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory Caracterizacion_de_producto_igual_al_primer_factor
imports Main
begin

context cancel_comm_monoid_add
begin

(* 1ª demostración *)

lemma "a + b = a ⟷ b = 0"
proof (rule iffI)
  assume "a + b = a"
  then have "a + b = a + 0"     by (simp only: add_0_right)
  then show "b = 0"             by (simp only: add_left_cancel)
next
  assume "b = 0"
  have "a + 0 = a"              by (simp only: add_0_right)
  with ‹b = 0› show "a + b = a" by (rule ssubst)
qed

(* 2ª demostración *)

lemma "a + b = a ⟷ b = 0"
proof
  assume "a + b = a"
  then have "a + b = a + 0" by simp
  then show "b = 0"         by simp
next
  assume "b = 0"
  have "a + 0 = a"          by simp
  then show "a + b = a"     using ‹b = 0› by simp
qed

(* 3ª demostración *)

lemma "a + b = a ⟷ b = 0"
proof -
  have "(a + b = a) ⟷ (a + b = a + 0)" by (simp only: add_0_right)
  also have "… ⟷ (b = 0)"              by (simp only: add_left_cancel)
  finally show "a + b = a ⟷ b = 0"     by this
qed

(* 4ª demostración *)

lemma "a + b = a ⟷ b = 0"
proof -
  have "(a + b = a) ⟷ (a + b = a + 0)" by simp
  also have "… ⟷ (b = 0)"              by simp
  finally show "a + b = a ⟷ b = 0"     .
qed

(* 5ª demostración *)

lemma "a + b = a ⟷ b = 0"
  by (simp only: add_cancel_left_right)

(* 6ª demostración *)

lemma "a + b = a ⟷ b = 0"
  by auto

end

end

theory Caracterizacion_de_producto_igual_al_primer_factor

imports Main

begin

context cancel_comm_monoid_add

begin

(* 1ª demostración *)

lemma "a + b = a ⟷ b = 0"

proof (rule iffI)

assume "a + b = a"

then have "a + b = a + 0" by (simp only: add_0_right)

then show "b = 0" by (simp only: add_left_cancel)

assume "b = 0"

have "a + 0 = a" by (simp only: add_0_right)

with ‹b = 0› show "a + b = a" by (rule ssubst)

qed

(* 2ª demostración *)

lemma "a + b = a ⟷ b = 0"

proof

assume "a + b = a"

then have "a + b = a + 0" by simp

then show "b = 0" by simp

assume "b = 0"

have "a + 0 = a" by simp

then show "a + b = a" using ‹b = 0› by simp

qed

(* 3ª demostración *)

lemma "a + b = a ⟷ b = 0"

proof -

have "(a + b = a) ⟷ (a + b = a + 0)" by (simp only: add_0_right)

also have "… ⟷ (b = 0)" by (simp only: add_left_cancel)

finally show "a + b = a ⟷ b = 0" by this

qed

(* 4ª demostración *)

lemma "a + b = a ⟷ b = 0"

proof -

have "(a + b = a) ⟷ (a + b = a + 0)" by simp

also have "… ⟷ (b = 0)" by simp

finally show "a + b = a ⟷ b = 0" .

qed

(* 5ª demostración *)

lemma "a + b = a ⟷ b = 0"

by (simp only: add_cancel_left_right)

(* 6ª demostración *)

lemma "a + b = a ⟷ b = 0"

by auto

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Unicidad de inversos en monoides conmutativos

PorJosé A. Alonso 2 julio 202123 junio 2021

Demostrar que en los monoides conmutativos, si un elemento tiene un inverso por la derecha, dicho inverso es único.

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

import algebra.group.basic

variables {M : Type} [comm_monoid M]
variables {x y z : M}

example
  (hy : x * y = 1)
  (hz : x * z = 1)
  : y = z :=
sorry

import algebra.group.basic

variables {M : Type} [comm_monoid M]

variables {x y z : M}

example

(hy : x * y = 1)

(hz : x * z = 1)

: y = z :=

sorry

[expand title=»Soluciones con Lean»]

import algebra.group.basic

variables {M : Type} [comm_monoid M]
variables {x y z : M}

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

example
  (hy : x * y = 1)
  (hz : x * z = 1)
  : y = z :=
calc y = 1 * y       : (one_mul y).symm
   ... = (x * z) * y : congr_arg (* y) hz.symm
   ... = (z * x) * y : congr_arg (* y) (mul_comm x z)
   ... = z * (x * y) : mul_assoc z x y
   ... = z * 1       : congr_arg ((*) z) hy
   ... = z           : mul_one z

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

example
  (hy : x * y = 1)
  (hz : x * z = 1)
  : y = z :=
calc y = 1 * y       : by simp only [one_mul]
   ... = (x * z) * y : by simp only [hz]
   ... = (z * x) * y : by simp only [mul_comm]
   ... = z * (x * y) : by simp only [mul_assoc]
   ... = z * 1       : by simp only [hy]
   ... = z           : by simp only [mul_one]

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

example
  (hy : x * y = 1)
  (hz : x * z = 1)
  : y = z :=
calc y = 1 * y       : by simp
   ... = (x * z) * y : by simp [hz]
   ... = (z * x) * y : by simp [mul_comm]
   ... = z * (x * y) : by simp [mul_assoc]
   ... = z * 1       : by simp [hy]
   ... = z           : by simp

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

example
  (hy : x * y = 1)
  (hz : x * z = 1)
  : y = z :=
begin
  apply left_inv_eq_right_inv _ hz,
  rw mul_comm,
  exact hy,
end

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

example
  (hy : x * y = 1)
  (hz : x * z = 1)
  : y = z :=
left_inv_eq_right_inv (trans (mul_comm _ _) hy) hz

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

example
  (hy : x * y = 1)
  (hz : x * z = 1)
  : y = z :=
inv_unique hy hz

import algebra.group.basic

variables {M : Type} [comm_monoid M]

variables {x y z : M}

-- 1ª demostración

-- ===============

example

(hy : x * y = 1)

(hz : x * z = 1)

: y = z :=

calc y = 1 * y : (one_mul y).symm

... = (x * z) * y : congr_arg (* y) hz.symm

... = (z * x) * y : congr_arg (* y) (mul_comm x z)

... = z * (x * y) : mul_assoc z x y

... = z * 1 : congr_arg ((*) z) hy

... = z : mul_one z

-- 2ª demostración

-- ===============

example

(hy : x * y = 1)

(hz : x * z = 1)

: y = z :=

calc y = 1 * y : by simp only [one_mul]

... = (x * z) * y : by simp only [hz]

... = (z * x) * y : by simp only [mul_comm]

... = z * (x * y) : by simp only [mul_assoc]

... = z * 1 : by simp only [hy]

... = z : by simp only [mul_one]

-- 3ª demostración

-- ===============

example

(hy : x * y = 1)

(hz : x * z = 1)

: y = z :=

calc y = 1 * y : by simp

... = (x * z) * y : by simp [hz]

... = (z * x) * y : by simp [mul_comm]

... = z * (x * y) : by simp [mul_assoc]

... = z * 1 : by simp [hy]

... = z : by simp

-- 4ª demostración

-- ===============

example

(hy : x * y = 1)

(hz : x * z = 1)

: y = z :=

begin

apply left_inv_eq_right_inv _ hz,

rw mul_comm,

exact hy,

end

-- 5ª demostración

-- ===============

example

(hy : x * y = 1)

(hz : x * z = 1)

: y = z :=

left_inv_eq_right_inv (trans (mul_comm _ _) hy) hz

-- 6ª demostración

-- ===============

example

(hy : x * y = 1)

(hz : x * z = 1)

: y = z :=

inv_unique hy hz

Se puede interactuar con la prueba anterior en esta sesión con Lean,

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory Unicidad_de_inversos_en_monoides
imports Main
begin

context comm_monoid
begin

(* 1ª demostración *)

lemma
  assumes "x * y = 1"
          "x * z = 1"
  shows "y = z"
proof -
  have "y = 1 * y"            by (simp only: left_neutral)
  also have "… = (x * z) * y" by (simp only: ‹x * z = 1›)
  also have "… = (z * x) * y" by (simp only: commute)
  also have "… = z * (x * y)" by (simp only: assoc)
  also have "… = z * 1"       by (simp only: ‹x * y = 1›)
  also have "… = z"           by (simp only: right_neutral)
  finally show "y = z"        by this
qed

(* 2ª demostración *)

lemma
  assumes "x * y = 1"
          "x * z = 1"
  shows "y = z"
proof -
  have "y = 1 * y"            by simp
  also have "… = (x * z) * y" using assms(2) by simp
  also have "… = (z * x) * y" by simp
  also have "… = z * (x * y)" by simp
  also have "… = z * 1"       using assms(1) by simp
  also have "… = z"           by simp
  finally show "y = z"        by this
qed

(* 3ª demostración *)

lemma
  assumes "x * y = 1"
          "x * z = 1"
  shows "y = z"
  using assms
  by auto

end

end

theory Unicidad_de_inversos_en_monoides

imports Main

begin

context comm_monoid

begin

(* 1ª demostración *)

lemma

assumes "x * y = 1"

"x * z = 1"

shows "y = z"

proof -

have "y = 1 * y" by (simp only: left_neutral)

also have "… = (x * z) * y" by (simp only: ‹x * z = 1›)

also have "… = (z * x) * y" by (simp only: commute)

also have "… = z * (x * y)" by (simp only: assoc)

also have "… = z * 1" by (simp only: ‹x * y = 1›)

also have "… = z" by (simp only: right_neutral)

finally show "y = z" by this

qed

(* 2ª demostración *)

lemma

assumes "x * y = 1"

"x * z = 1"

shows "y = z"

proof -

have "y = 1 * y" by simp

also have "… = (x * z) * y" using assms(2) by simp

also have "… = (z * x) * y" by simp

also have "… = z * (x * y)" by simp

also have "… = z * 1" using assms(1) by simp

also have "… = z" by simp

finally show "y = z" by this

qed

(* 3ª demostración *)

lemma

assumes "x * y = 1"

"x * z = 1"

shows "y = z"

using assms

by auto

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]