En ℝ, |a| = |a – b + b|

Demostrar con Lean4 que en \(ℝ\), \(|a| = |a – b + b|\)

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

Read More «En ℝ, |a| = |a – b + b|»

Las funciones f(x,y) = (x + y)² y g(x,y) = x² + 2xy + y² son iguales

Demostrar con Lean4 que las funciones \(f(x,y) = (x + y)²\) y \(g(x,y) = x² + 2xy + y\)² son iguales.

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

Read More «Las funciones f(x,y) = (x + y)² y g(x,y) = x² + 2xy + y² son iguales»

La raíz cuadrada de 2 es irracional

Demostrar con Lean4 que la raíz cuadrada de 2 es irracional; es decir, que no existen \(m, n ∈ ℕ\) tales que \(m\) y \(n\) son coprimos (es decir, que no tienen factores comunes distintos de uno) y \(m² = 2n²\).

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

Read More «La raíz cuadrada de 2 es irracional»

Existen infinitos números primos

Demostrar con Lean4 que existen infinitos números primos.

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

Read More «Existen infinitos números primos»