∀ a b c ∈ ℝ, a(bc) = b(ac)
Demostrar con Lean4 que ∀ a b c ∈ ℝ, a * (b * c) = b * (a * c)
Para ello, completar la siguiente teoría de Lean4:
1 2 3 4 5 6 |
import Mathlib.Tactic import Mathlib.Data.Real.Basic example (a b c : ℝ) : a * (b * c) = b * (a * c) := by sorry |