Commit 2022-09-23 04:37 98cbfb45

View on Github →

chore(tactic/monotonicity/lemmas): Move lemmas to the correct places (#16509) A few lemmas were gathered in tactic.monotonicity.lemmas rather than the files they belong to. Generalize them, move them and fix their names.

Estimated changes

Modified src/algebra/order/ring.lean

added theorem lt_of_mul_lt_mul_of_nonpos_left

added theorem lt_of_mul_lt_mul_of_nonpos_right

Modified src/algebra/order/sub.lean

added theorem tsub_lt_tsub_left_of_le

Modified src/analysis/calculus/taylor.lean

Modified src/analysis/inner_product_space/projection.lean

Modified src/data/bitvec/basic.lean

Modified src/number_theory/liouville/liouville_constant.lean

Modified src/tactic/monotonicity/lemmas.lean

deleted theorem lt_of_mul_lt_mul_neg_right

deleted theorem mul_mono_nonneg

deleted theorem mul_mono_nonpos

deleted theorem nat.sub_mono_left_strict

deleted theorem nat.sub_mono_right_strict