14 julio 2023 – Calculemus

Si ab = cd y e = f, entonces a(be) = c(df)

PorJosé A. Alonso 14 julio 202319 julio 2023

Demostrar con Lean4 que si ab = cd y e = f, entonces a(be) = c(df)

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

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

example
  (a b c d e f : ℝ)
  (h1 : a * b = c * d)
  (h2 : e = f)
  : a * (b * e) = c * (d * f) :=
by sorry

import Mathlib.Tactic

import Mathlib.Data.Real.Basic

example

(a b c d e f : ℝ)

(h1 : a * b = c * d)

(h2 : e = f)

: a * (b * e) = c * (d * f) :=

by sorry