19 julio 2023 – Calculemus

(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