Commit 2023-11-22 05:01 f70d883a

View on Github →

feat: add div/mod/dvd on Nat/Int to norm_num (#8534)

Estimated changes

Modified .vscode/settings.json

Modified Mathlib.lean

Modified Mathlib/Tactic.lean

Modified Mathlib/Tactic/NormNum.lean

Modified Mathlib/Tactic/NormNum/Basic.lean

added theorem Mathlib.Meta.NormNum.IsInt.raw_refl

modified def Mathlib.Meta.NormNum.evalNatDiv

added def Mathlib.Meta.NormNum.evalNatDvd

added theorem Mathlib.Meta.NormNum.isNat_dvd_false

added theorem Mathlib.Meta.NormNum.isNat_dvd_true

Created Mathlib/Tactic/NormNum/DivMod.lean

added def Mathlib.Meta.NormNum.evalIntDvd

added theorem Mathlib.Meta.NormNum.isInt_dvd_false

added theorem Mathlib.Meta.NormNum.isInt_dvd_true

added theorem Mathlib.Meta.NormNum.isInt_ediv

added theorem Mathlib.Meta.NormNum.isInt_ediv_neg

added theorem Mathlib.Meta.NormNum.isInt_ediv_zero

added theorem Mathlib.Meta.NormNum.isInt_emod

added theorem Mathlib.Meta.NormNum.isInt_emod_neg

added theorem Mathlib.Meta.NormNum.isInt_emod_zero

added theorem Mathlib.Meta.NormNum.isNat_neg_of_isNegNat

Deleted Mathlib/Tactic/NormNum/Mod.lean

deleted theorem Mathlib.Meta.NormNum.isInt_emod

deleted theorem Mathlib.Meta.NormNum.isInt_emod_neg

deleted theorem Mathlib.Meta.NormNum.isInt_refl

deleted theorem Mathlib.Meta.NormNum.isNat_neg_of_isNegNat

Modified Mathlib/Tactic/NormNum/Result.lean

Modified Mathlib/Tactic/ReduceModChar.lean

modified theorem Tactic.ReduceModChar.CharP.isInt_of_mod

Modified test/norm_num.lean

Modified test/norm_num_ext.lean