agosto 2022 – Calculemus

Si R es un anillo y a, b, c ∈ R tales que a + b = a + c, entonces b = c.

PorJosé A. Alonso 31 agosto 202211 septiembre 2022

Demostrar que si R es un anillo y a, b, c ∈ R tales que

   a + b = a + c

1	a + b = a + c

entonces

   b = c

b = c

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

import algebra.ring
import tactic

variables {R : Type*} [ring R]
variables {a b c : R}

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

import algebra.ring

import tactic

variables {R : Type*} [ring R]

variables {a b c : R}

example

(h : a + b = a + c)

: b = c :=

sorry

Si R es un anillo y a, b ∈ R, entonces (a + b) + -b = a

PorJosé A. Alonso 30 agosto 202211 septiembre 2022

Demostrar que si R es un anillo, entonces

   ∀ a b : R, (a + b) + -b = a

1	∀ a b : R, (a + b) + -b = a

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

import algebra.ring

variables {R : Type*} [ring R]
variables a b : R

example : (a + b) + -b = a :=
sorry

import algebra.ring

variables {R : Type*} [ring R]

variables a b : R

example : (a + b) + -b = a :=

sorry

Si R es un anillo y a, b ∈ R, entonces -a + (a + b) = b

PorJosé A. Alonso 29 agosto 202211 septiembre 2022

En Lean, se declara que R es un anillo mediante la expresión

   variables {R : Type*} [ring R]

1	variables {R : Type*} [ring R]

y, como consecuencia, se tienen los siguientes axiomas

   add_assoc    : ∀ a b c : R, (a + b) + c = a + (b + c)
   add_comm     : ∀ a b : R,   a + b = b + a
   zero_add     : ∀ a : R,     0 + a = a
   add_left_neg : ∀ a : R,     -a + a = 0
   mul_assoc    : ∀ a b c : R, a * b * c = a * (b * c)
   mul_one      : ∀ a : R,     a * 1 = a
   one_mul      : ∀ a : R,     1 * a = a
   mul_add      : ∀ a b c : R, a * (b + c) = a * b + a * c
   add_mul      : ∀ a b c : R, (a + b) * c = a * c + b * c

add_assoc : ∀ a b c : R, (a + b) + c = a + (b + c)

add_comm : ∀ a b : R, a + b = b + a

zero_add : ∀ a : R, 0 + a = a

add_left_neg : ∀ a : R, -a + a = 0

mul_assoc : ∀ a b c : R, a * b * c = a * (b * c)

mul_one : ∀ a : R, a * 1 = a

one_mul : ∀ a : R, 1 * a = a

mul_add : ∀ a b c : R, a * (b + c) = a * b + a * c

add_mul : ∀ a b c : R, (a + b) * c = a * c + b * c

Demostrar que si R es un anillo, entonces

   ∀ a b : R, -a + (a + b) = b

1	∀ a b : R, -a + (a + b) = b

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

import algebra.ring
import tactic

variables {R : Type*} [ring R]
variables a b : R

example
  : -a + (a + b) = b :=
sorry

import algebra.ring

import tactic

variables {R : Type*} [ring R]

variables a b : R

example

: -a + (a + b) = b :=

sorry

Si a y b son números reales, entonces (a + b) * (a – b) = a^2 – b^2

PorJosé A. Alonso 26 agosto 202211 septiembre 2022

Demostrar que si a y b son números reales, entonces

(a + b) * (a - b) = a^2 - b^2

1	(a + b) * (a - b) = a^2 - b^2

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

import data.real.basic

variables a b c d : ℝ

example : (a + b) * (a - b) = a^2 - b^2 :=
sorry

import data.real.basic

variables a b c d : ℝ

example : (a + b) * (a - b) = a^2 - b^2 :=

sorry

Si a, b, c y d son números reales, entonces (a + b) * (c + d) = a * c + a * d + b * c + b * d

PorJosé A. Alonso 25 agosto 202211 septiembre 2022

Demostrar que si a, b, c y d son números reales, entonces

(a + b) * (c + d) = a * c + a * d + b * c + b * d

1	(a + b) * (c + d) = a * c + a * d + b * c + b * d

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

import data.real.basic

variables a b c d : ℝ

example
  : (a + b) * (c + d) = a * c + a * d + b * c + b * d :=
sorry

import data.real.basic

variables a b c d : ℝ

example

: (a + b) * (c + d) = a * c + a * d + b * c + b * d :=

sorry