24 julio 2023 – Calculemus

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