agosto 2022 – Página 2

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

PorJosé A. Alonso 24 agosto 202211 septiembre 2022

Demostrar 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 Lean:

import data.real.basic

variables a b : ℝ

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

import data.real.basic

variables a b : ℝ

example :

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

sorry

PorJosé A. Alonso 23 agosto 202211 septiembre 2022

Demostrar que si a, b, c, d, e y f son números reales tales que

   a * b = c * d
   e = f

1 2	a * b = c * d e = f

Entonces,

   a * (b * e) = c * (d * f)

1	a * (b * e) = c * (d * f)

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

import data.real.basic

variables a b c d e f : ℝ

example
  (h1 : a * b = c * d)
  (h2 : e = f)
  : a * (b * e) = c * (d * f) :=

import data.real.basic

variables a b c d e f : ℝ

example

(h1 : a * b = c * d)

(h2 : e = f)

: a * (b * e) = c * (d * f) :=

PorJosé A. Alonso 22 agosto 202211 septiembre 2022

Demostrar que los números reales tienen la siguiente propiedad

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

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

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

import data.real.basic

variables a b c : ℝ

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

import data.real.basic

variables a b c : ℝ

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

sorry

PorJosé A. Alonso 21 agosto 202211 septiembre 2022

Demostrar que los productos de los números naturales por números pares son pares.

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

import data.nat.parity
import tactic

open nat

example : ∀ m n : ℕ, even n → even (m * n) :=
sorry

import data.nat.parity

import tactic

open nat

example : ∀ m n : ℕ, even n → even (m * n) :=

sorry