13 julio 2023 – Calculemus

∀ a b c ∈ ℝ, a(bc) = b(ac)

PorJosé A. Alonso 13 julio 202319 julio 2023

Demostrar con Lean4 que ∀ a b c ∈ ℝ, a * (b * c) = b * (a * c)

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

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

example
  (a b c : ℝ) : a * (b * c) = b * (a * c) :=
by sorry

import Mathlib.Tactic

import Mathlib.Data.Real.Basic

example

(a b c : ℝ) : a * (b * c) = b * (a * c) :=

by sorry