18 julio 2023 – Calculemus

Si c = ba-d y d = ab, entonces c = 0

PorJosé A. Alonso 18 julio 202319 julio 2023

Demostrar con Lean4 que si a, b, c y d son números reales tales

   c = b * a - d
   d = a * b

1 2	c = b * a - d d = a * b

entonces

   c = 0

c = 0

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

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

example
  (a b c d : ℝ)
  (h1 : c = b * a - d)
  (h2 : d = a * b)
  : c = 0 :=
by sorry

import Mathlib.Data.Real.Basic

import Mathlib.Tactic

example

(a b c d : ℝ)

(h1 : c = b * a - d)

(h2 : d = a * b)

: c = 0 :=

by sorry