José A. Alonso

Si R es un anillo, entonces -0 = 0

PorJosé A. Alonso 8 septiembre 202211 septiembre 2022

Demostrar que si R es un anillo, entonces

-0 = 0

-0 = 0

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

import algebra.ring

variables {R : Type*} [ring R]

example : (-0 : R) = 0 :=
sorry

import algebra.ring

variables {R : Type*} [ring R]

example : (-0 : R) = 0 :=

sorry

Si R es un anillo y a,b∈R tales que a+b=0, entonces a=-b

PorJosé A. Alonso 7 septiembre 202211 septiembre 2022

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

a + b = 0

a + b = 0

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
  (h : a + b = 0)
  : a = -b :=
sorry

import algebra.ring

variables {R : Type*} [ring R]

variables {a b : R}

example

(h : a + b = 0)

: a = -b :=

sorry

Si R es un anillo y a,b∈R tales que a+b=0, entonces -a=b

PorJosé A. Alonso 6 septiembre 202211 septiembre 2022

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

a + b = 0

a + b = 0

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
  (h : a + b = 0)
  : -a = b :=
sorry

import algebra.ring

variables {R : Type*} [ring R]

variables {a b : R}

example

(h : a + b = 0)

: -a = b :=

sorry

Si R es un anillo y a ∈ R, entonces 0 * a = 0

PorJosé A. Alonso 5 septiembre 202211 septiembre 2022

Demostrar que si R es un anillo y a ∈ R, entonces

0 * a = 0.

1	0 * a = 0.

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

import algebra.ring

variables {R : Type*} [ring R]
variable (a : R)

example : 0 * a = 0 :=
sorry

import algebra.ring

variables {R : Type*} [ring R]

variable (a : R)

example : 0 * a = 0 :=

sorry

Si R es un anillo y a ∈ R, entonces a * 0 = 0

PorJosé A. Alonso 2 septiembre 202211 septiembre 2022

Demostrar que Si R es un anillo y a ∈ R, entonces

a * 0 = 0

a * 0 = 0

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

import algebra.ring

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

example : a * 0 = 0 :=
sorry

import algebra.ring

variables {R : Type*} [ring R]

variable a : R

example : a * 0 = 0 :=

sorry

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

PorJosé A. Alonso 1 septiembre 202211 septiembre 2022

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

   a + b = c + b

1	a + b = c + b

entonces

   a = c

a = 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 = c + b)
  : a = c :=
sorry

import algebra.ring

import tactic

variables {R : Type*} [ring R]

variables {a b c : R}

example

(h : a + b = c + b)

: a = c :=

sorry

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