Def Mathlib.Meta.NormNum.evalNNRatCast

Modification history

2026-06-10 19:34

Mathlib/Tactic/NormNum/Inv.lean

feat(Tactic): generalize ofScientific NormNum extension to `DivisionSemiring` (#34805)

Added Mathlib.Meta.NormNum.evalNNRatCast View on Github →