Commit 2026-06-10 19:34 4cae50e2

View on Github →

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

Estimated changes

Modified Mathlib/Algebra/Field/Rat.lean

added theorem NNRat.divNat_eq_div

added theorem NNRatCast.ofScientific_eq_ite

Modified Mathlib/Tactic/NormNum/Inv.lean

added def Mathlib.Meta.NormNum.evalNNRatCast

added def Mathlib.Meta.NormNum.evalNNRatDivNat

added theorem Mathlib.Meta.NormNum.isNNRat_divNat

added theorem Mathlib.Meta.NormNum.isNNRat_nnratCast

added theorem Mathlib.Meta.NormNum.isNat_nnratCast

Modified Mathlib/Tactic/NormNum/OfScientific.lean

modified theorem Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true

modified theorem Mathlib.Meta.NormNum.isNat_ofScientific_of_false

Modified MathlibTest/Tactic/NormNum/Basic.lean