17 julio 2023 – Calculemus

Si bc = ef, entonces ((ab)c)d = ((ae)f)d

PorJosé A. Alonso 17 julio 202319 julio 2023

Demostrar con Lean4 que si bc = ef, entonces ((ab)c)d = ((ae)f)d.

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

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

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

import Mathlib.Data.Real.Basic

import Mathlib.Tactic

example

(a b c d e f : ℝ)

(h : b * c = e * f)

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

by sorry