Theorem Mathlib.Meta.NormNum.isNat_nnratCast

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.isNat_nnratCastView on Github →