Def Mathlib.Meta.NormNum.Result.mul

Modification history

2025-08-20 15:48
Mathlib/Tactic/NormNum/Basic.lean
refactor(Tactic/NormNum): expose the derive API for known expressions directly (#28621) …
Added Mathlib.Meta.NormNum.Result.mulView on Github →