Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-05-23 04:50
6292b8e9
View on Github →
feat: norm num extension for division and succ of naturals (
#4090
)
Estimated changes
Modified
Mathlib/Tactic/NormNum/Basic.lean
added
def
Mathlib.Meta.NormNum.evalNatDiv
added
def
Mathlib.Meta.NormNum.evalNatSucc
added
theorem
Mathlib.Meta.NormNum.isNat_natDiv
added
theorem
Mathlib.Meta.NormNum.isNat_natSucc
Modified
test/norm_num.lean