Commit 2022-11-20 09:01 afd0c163

View on Github →

feat: port algebra.order.monoid.lemmas (#608) I had to change one proof due to a to_additive issue, see Zulip. mathlib3 sha: 7cca171008afb30576d2d4c51173700a780c23d0 Diff from mathport output

depends on: #591

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Order/Group.lean

Modified Mathlib/Algebra/Order/Monoid.lean

Created Mathlib/Algebra/Order/Monoid/Lemmas.lean

added theorem Antitone.const_mul'

added theorem Antitone.mul'

added theorem Antitone.mul_const'

added theorem Antitone.mul_strict_anti'

added theorem AntitoneOn.const_mul'

added theorem AntitoneOn.mul'

added theorem AntitoneOn.mul_const'

added theorem AntitoneOn.mul_strict_anti'

added theorem Contravariant.MulLeCancellable

added def Contravariant.toLeftCancelSemigroup

added def Contravariant.toRightCancelSemigroup

added theorem Left.mul_eq_mul_iff_eq_and_eq

added theorem Left.mul_le_one

added theorem Left.mul_lt_mul

added theorem Left.mul_lt_one'

added theorem Left.mul_lt_one

added theorem Left.mul_lt_one_of_le_of_lt

added theorem Left.mul_lt_one_of_lt_of_le

added theorem Left.one_le_mul

added theorem Left.one_lt_mul'

added theorem Left.one_lt_mul

added theorem Left.one_lt_mul_of_le_of_lt

added theorem Left.one_lt_mul_of_lt_of_le

added theorem Monotone.const_mul'

added theorem Monotone.mul'

added theorem Monotone.mul_const'

added theorem Monotone.mul_strict_mono'

added theorem MonotoneOn.const_mul'

added theorem MonotoneOn.mul'

added theorem MonotoneOn.mul_const'

added theorem MonotoneOn.mul_strict_mono'

added def MulLeCancellable

added theorem Right.mul_eq_mul_iff_eq_and_eq

added theorem Right.mul_le_one

added theorem Right.mul_lt_mul

added theorem Right.mul_lt_one'

added theorem Right.mul_lt_one

added theorem Right.mul_lt_one_of_le_of_lt

added theorem Right.mul_lt_one_of_lt_of_le

added theorem Right.one_le_mul

added theorem Right.one_lt_mul'

added theorem Right.one_lt_mul

added theorem Right.one_lt_mul_of_le_of_lt

added theorem Right.one_lt_mul_of_lt_of_le

added theorem StrictAnti.const_mul'

added theorem StrictAnti.mul'

added theorem StrictAnti.mul_antitone'

added theorem StrictAnti.mul_const'

added theorem StrictAntiOn.const_mul'

added theorem StrictAntiOn.mul'

added theorem StrictAntiOn.mul_antitone'

added theorem StrictAntiOn.mul_const'

added theorem StrictMono.const_mul'

added theorem StrictMono.mul'

added theorem StrictMono.mul_const'

added theorem StrictMono.mul_monotone'

added theorem StrictMonoOn.const_mul'

added theorem StrictMonoOn.mul'

added theorem StrictMonoOn.mul_const'

added theorem StrictMonoOn.mul_monotone'

added theorem cmp_mul_left'

added theorem cmp_mul_right'

added theorem eq_one_of_mul_le_one_left

added theorem eq_one_of_mul_le_one_right

added theorem eq_one_of_one_le_mul_left

added theorem eq_one_of_one_le_mul_right

added theorem exists_square_le

added theorem le_mul_iff_one_le_left'

added theorem le_mul_iff_one_le_right'

added theorem le_mul_of_le_mul_left

added theorem le_mul_of_le_mul_right

added theorem le_mul_of_le_of_one_le

added theorem le_mul_of_one_le_left'

added theorem le_mul_of_one_le_of_le

added theorem le_mul_of_one_le_right'

added theorem le_of_le_mul_of_le_one_left

added theorem le_of_le_mul_of_le_one_right

added theorem le_of_mul_le_mul_left'

added theorem le_of_mul_le_mul_right'

added theorem le_of_mul_le_of_one_le_left

added theorem le_of_mul_le_of_one_le_right

added theorem le_one_of_mul_le_left

added theorem le_one_of_mul_le_right

added theorem lt_mul_iff_one_lt_left'

added theorem lt_mul_iff_one_lt_right'

added theorem lt_mul_of_le_of_one_lt

added theorem lt_mul_of_lt_mul_left

added theorem lt_mul_of_lt_mul_right

added theorem lt_mul_of_lt_of_one_le

added theorem lt_mul_of_lt_of_one_lt'

added theorem lt_mul_of_lt_of_one_lt

added theorem lt_mul_of_one_le_of_lt

added theorem lt_mul_of_one_lt_left'

added theorem lt_mul_of_one_lt_of_le

added theorem lt_mul_of_one_lt_of_lt'

added theorem lt_mul_of_one_lt_of_lt

added theorem lt_mul_of_one_lt_right'

added theorem lt_of_lt_mul_of_le_one_left

added theorem lt_of_lt_mul_of_le_one_right

added theorem lt_of_mul_lt_mul_left'

added theorem lt_of_mul_lt_mul_right'

added theorem lt_of_mul_lt_of_one_le_left

added theorem lt_of_mul_lt_of_one_le_right

added theorem lt_one_of_mul_lt_left

added theorem lt_one_of_mul_lt_right

added theorem mul_eq_one_iff'

added theorem mul_le_cancellable_one

added theorem mul_le_iff_le_one_left'

added theorem mul_le_iff_le_one_right'

added theorem mul_le_mul'

added theorem mul_le_mul_iff_left

added theorem mul_le_mul_iff_right

added theorem mul_le_mul_left'

added theorem mul_le_mul_right'

added theorem mul_le_mul_three

added theorem mul_le_of_le_of_le_one

added theorem mul_le_of_le_one_left'

added theorem mul_le_of_le_one_of_le

added theorem mul_le_of_le_one_right'

added theorem mul_le_of_mul_le_left

added theorem mul_le_of_mul_le_right

added theorem mul_left_cancel''

added theorem mul_lt_iff_lt_one_left'

added theorem mul_lt_iff_lt_one_right'

added theorem mul_lt_mul_iff_left

added theorem mul_lt_mul_iff_right

added theorem mul_lt_mul_left'

added theorem mul_lt_mul_of_le_of_lt

added theorem mul_lt_mul_of_lt_of_le

added theorem mul_lt_mul_of_lt_of_lt

added theorem mul_lt_mul_right'

added theorem mul_lt_of_le_of_lt_one

added theorem mul_lt_of_le_one_of_lt

added theorem mul_lt_of_lt_of_le_one

added theorem mul_lt_of_lt_of_lt_one'

added theorem mul_lt_of_lt_of_lt_one

added theorem mul_lt_of_lt_one_left'

added theorem mul_lt_of_lt_one_of_le

added theorem mul_lt_of_lt_one_of_lt'

added theorem mul_lt_of_lt_one_of_lt

added theorem mul_lt_of_lt_one_right'

added theorem mul_lt_of_mul_lt_left

added theorem mul_lt_of_mul_lt_right

added theorem mul_right_cancel''

added theorem one_le_of_le_mul_left

added theorem one_le_of_le_mul_right

added theorem one_lt_of_lt_mul_left

added theorem one_lt_of_lt_mul_right

Deleted Mathlib/Algebra/Order/MonoidLemmas.lean

deleted theorem le_of_mul_le_mul_left'

deleted theorem lt_of_mul_lt_mul_left'

deleted theorem mul_le_mul_iff_left

deleted theorem mul_le_mul_iff_right

deleted theorem mul_le_mul_left'

deleted theorem mul_lt_mul_iff_left

deleted theorem mul_lt_mul_iff_right

deleted theorem mul_lt_mul_left'

Modified Mathlib/Init/Algebra/Order.lean

Modified Mathlib/Tactic/Positivity/Basic.lean

deleted theorem add_nonneg

deleted theorem add_pos

deleted theorem lt_add_of_le_of_pos

deleted theorem lt_add_of_pos_of_le