25 julio 2023 – Calculemus

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