julio 2023 – Calculemus

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

PorJosé A. Alonso 31 julio 202323 julio 2023

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

   variable {R : Type _} [Ring R]

1	variable {R : Type _} [Ring R]

Como consecuencia, se tiene 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 + b) + -b = a

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

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

import Mathlib.Algebra.Ring.Defs

variable {R : Type _} [Ring R]
variable (a b : R)

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

import Mathlib.Algebra.Ring.Defs

variable {R : Type _} [Ring R]

variable (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 28 julio 202329 julio 2023

Demostrar en Lean4 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 Lean4:

import Mathlib.Algebra.Ring.Defs

variable {R : Type _} [Ring R]
variable (a b : R)

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

import Mathlib.Algebra.Ring.Defs

variable {R : Type _} [Ring R]

variable (a b : R)

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

sorry

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

PorJosé A. Alonso 27 julio 202329 julio 2023

Demostrar con Lean4 que si \(R\) es un anillo, entonces

   ∀ a : R, a + -a = 0

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

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

import Mathlib.Algebra.Ring.Defs

variable {R : Type _} [Ring R]
variable (a : R)

example : a + -a = 0 :=
sorry

import Mathlib.Algebra.Ring.Defs

variable {R : Type _} [Ring R]

variable (a : R)

example : a + -a = 0 :=

sorry

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

PorJosé A. Alonso 26 julio 202321 julio 2023

En Lean4, se declara que \(R\) es un anillo mediante la expresión

   variable {R : Type _} [Ring R]

1	variable {R : Type _} [Ring R]

Como consecuencia, se tiene 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 : R, a + 0 = a

1	∀ a : R, a + 0 = a

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

import Mathlib.Algebra.Ring.Defs

variable {R : Type _} [Ring R]
variable (a : R)

example : a + 0 = a :=
sorry

import Mathlib.Algebra.Ring.Defs

variable {R : Type _} [Ring R]

variable (a : R)

example : a + 0 = a :=

sorry

Si a+b = c, entonces (a+b)(a+b) = ac+ bc

PorJosé A. Alonso 25 julio 202321 julio 2023

Demostrar con Lean4 que si a, b y c son números reales tales que

   a + b = c,

1	a + b = c,

entonces

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

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

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

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

variable (a b c : ℝ)

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

import Mathlib.Data.Real.Basic

import Mathlib.Tactic

variable (a b c : ℝ)

example

(h : a + b = c)

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

sorry

Si c = da+b y b = ad, entonces c = 2ad

PorJosé A. Alonso 24 julio 202321 julio 2023

Demostrar con Lean4 que si a, b, c y d son números reales tales que

   c = d * a + b
   b = a * d

1 2	c = d * a + b b = a * d

entonces

   c = 2 * a * d

1	c = 2 * a * d

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

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

variable (a b c d : ℝ)

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

import Mathlib.Data.Real.Basic

import Mathlib.Tactic

variable (a b c d : ℝ)

example

(h1 : c = d * a + b)

(h2 : b = a * d)

: c = 2 * a * d :=

sorry

(a+b)(a-b) = a²-b²

PorJosé A. Alonso 21 julio 202321 julio 2023

Demostrar con Lean4 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 Lean4:

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

variable (a b : ℝ)

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

import Mathlib.Data.Real.Basic

import Mathlib.Tactic

variable (a b : ℝ)

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

sorry

(a + b) (c + d) = ac + ad + bc + bd

PorJosé A. Alonso 20 julio 202319 julio 2023

Demostrar con Lean4 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 Lean4:

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

variable (a b c d : ℝ)

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

import Mathlib.Data.Real.Basic

import Mathlib.Tactic

variable (a b c d : ℝ)

example

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

sorry

(a + b)(a + b) = aa + 2ab + bb

PorJosé A. Alonso 19 julio 202319 julio 2023

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

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

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

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

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

variable (a b c : ℝ)

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

import Mathlib.Data.Real.Basic

import Mathlib.Tactic

variable (a b c : ℝ)

example :

(a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=

sorry

Si c = ba-d y d = ab, entonces c = 0

PorJosé A. Alonso 18 julio 202319 julio 2023

Demostrar con Lean4 que si a, b, c y d son números reales tales

   c = b * a - d
   d = a * b

1 2	c = b * a - d d = a * b

entonces

   c = 0

c = 0

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

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

example
  (a b c d : ℝ)
  (h1 : c = b * a - d)
  (h2 : d = a * b)
  : c = 0 :=
by sorry

import Mathlib.Data.Real.Basic

import Mathlib.Tactic

example

(a b c d : ℝ)

(h1 : c = b * a - d)

(h2 : d = a * b)

: c = 0 :=

by sorry