Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-11 03:45 3348bed9

View on Github →

chore(tactic/linarith): remove unneeded code (#16791) Removes some unneeded lemmas (and consequently unneeded imports) in tactic/linarith/lemmas.lean, in preparation for porting.

Estimated changes

Modified src/algebra/order/ring.lean

Modified src/data/int/basic.lean

Modified src/tactic/linarith/lemmas.lean

deleted theorem linarith.int.coe_nat_bit0

deleted theorem linarith.int.coe_nat_bit0_mul

deleted theorem linarith.int.coe_nat_bit1

deleted theorem linarith.int.coe_nat_bit1_mul

deleted theorem linarith.int.coe_nat_mul_bit0

deleted theorem linarith.int.coe_nat_mul_bit1

deleted theorem linarith.int.coe_nat_mul_one

deleted theorem linarith.int.coe_nat_mul_zero

deleted theorem linarith.int.coe_nat_one_mul

deleted theorem linarith.int.coe_nat_zero_mul

deleted theorem linarith.nat_eq_subst

deleted theorem linarith.nat_le_subst

deleted theorem linarith.nat_lt_subst