Commit 2023-09-12 05:28 6de53297

View on Github →

chore: further refactors of prerequisites of norm_num (#7097)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Order/Invertible.lean

Modified Mathlib/Algebra/Order/Nonneg/Ring.lean

Modified Mathlib/Data/Int/Basic.lean

added theorem Int.cast_mul

Modified Mathlib/Data/Int/Cast/Lemmas.lean

deleted theorem Int.cast_mul

Modified Mathlib/Data/Int/Dvd/Basic.lean

Modified Mathlib/Data/Int/Lemmas.lean

Modified Mathlib/Data/Nat/Cast/Basic.lean

deleted theorem Nat.cast_add_one_pos

deleted theorem Nat.cast_max

deleted theorem Nat.cast_min

deleted theorem Nat.cast_nonneg'

deleted theorem Nat.cast_nonneg

deleted theorem Nat.cast_pos'

deleted theorem Nat.cast_pos

deleted theorem Nat.cast_tsub

deleted theorem Nat.mono_cast

deleted theorem ofDual_natCast

deleted theorem ofLex_natCast

deleted theorem toDual_natCast

deleted theorem toLex_natCast

Modified Mathlib/Data/Nat/Cast/Order.lean

added theorem Nat.cast_add_one_pos

added theorem Nat.cast_max

added theorem Nat.cast_min

added theorem Nat.cast_nonneg'

added theorem Nat.cast_nonneg

added theorem Nat.cast_pos'

added theorem Nat.cast_pos

added theorem Nat.cast_tsub

added theorem Nat.mono_cast

Created Mathlib/Data/Nat/Cast/Synonym.lean

added theorem ofDual_natCast

added theorem ofLex_natCast

added theorem toDual_natCast

added theorem toLex_natCast

Modified Mathlib/Data/Rat/Defs.lean

Modified Mathlib/Data/Real/ENatENNReal.lean

Modified Mathlib/Tactic/NormNum/Basic.lean

deleted theorem Mathlib.Meta.NormNum.Rat.invOf_denom_swap

deleted def Mathlib.Meta.NormNum.evalMkRat

deleted theorem Mathlib.Meta.NormNum.isInt_le_false

deleted theorem Mathlib.Meta.NormNum.isInt_le_true

deleted theorem Mathlib.Meta.NormNum.isInt_lt_false

deleted theorem Mathlib.Meta.NormNum.isInt_lt_true

deleted theorem Mathlib.Meta.NormNum.isNat_eq_false

deleted theorem Mathlib.Meta.NormNum.isNat_le_true

deleted theorem Mathlib.Meta.NormNum.isNat_lt_false

deleted theorem Mathlib.Meta.NormNum.isRat_mkRat

Modified Mathlib/Tactic/NormNum/Eq.lean

added theorem Mathlib.Meta.NormNum.Rat.invOf_denom_swap

added theorem Mathlib.Meta.NormNum.isNat_eq_false

Modified Mathlib/Tactic/NormNum/Ineq.lean

added theorem Mathlib.Meta.NormNum.isInt_le_false

added theorem Mathlib.Meta.NormNum.isInt_le_true

added theorem Mathlib.Meta.NormNum.isInt_lt_false

added theorem Mathlib.Meta.NormNum.isInt_lt_true

added theorem Mathlib.Meta.NormNum.isNat_le_true

added theorem Mathlib.Meta.NormNum.isNat_lt_false

Modified Mathlib/Tactic/NormNum/Inv.lean

added def Mathlib.Meta.NormNum.evalMkRat

added theorem Mathlib.Meta.NormNum.isRat_mkRat