Commuting two price scale factors
ProvedWorkbookSource.problem_41109lean-workbooksource-checked
For any real price ,
Source: InternLM Lean-Workbook, record lean_workbook_41109 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.
Preamble
import Mathlib open Real Nat
Formal statement
theorem WorkbookSource.problem_41109 (p : ℝ) : p * 0.9 * 1.2 = p * 1.2 * 0.9 := by sorry
Source