Commit 2022-11-23 19:15 de92e20c

View on Github →

feat: port Algebra.Order.Ring.Lemmas (#482) mathlib3 hash: 7cca171008afb30576d2d4c51173700a780c23d0 FIXME: local notation doesn't work, had to make just notation and turn off quotPrecheck

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Order/Ring.lean

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

added theorem Left.lt_mul_of_lt_of_one_le_of_nonneg

added theorem Left.mul_le_one_of_le_of_le

added theorem Left.mul_lt_of_le_of_lt_one_of_pos

added theorem Left.mul_lt_of_lt_of_le_one_of_nonneg

added theorem Left.mul_nonneg

added theorem Left.mul_pos

added theorem Left.neg_of_mul_neg_left

added theorem Left.neg_of_mul_neg_right

added theorem Left.one_le_mul_of_le_of_le

added theorem Left.one_lt_mul_of_le_of_lt_of_pos

added theorem MulPosMono.toMulPosStrictMono

added theorem MulPosMono.to_mul_pos_reflect_lt

added theorem MulPosMonoRev.to_mul_pos_strict_mono

added theorem MulPosReflectLT.toMulPosMonoRev

added theorem MulPosReflectLT.to_mul_pos_mono

added theorem PosMulMono.toPosMulStrictMono

added theorem PosMulMono.to_pos_mul_reflect_lt

added theorem PosMulMonoRev.to_pos_mul_strict_mono

added theorem PosMulReflectLT.toPosMulMonoRev

added theorem PosMulReflectLT.to_pos_mul_mono

added theorem Right.mul_le_one_of_le_of_le

added theorem Right.mul_lt_one_of_le_of_lt_of_nonneg

added theorem Right.mul_lt_one_of_lt_of_le_of_pos

added theorem Right.mul_nonneg

added theorem Right.mul_pos

added theorem Right.neg_of_mul_neg_left

added theorem Right.neg_of_mul_neg_right

added theorem Right.one_le_mul_of_le_of_le

added theorem Right.one_lt_mul_of_le_of_lt_of_nonneg

added theorem Right.one_lt_mul_of_lt_of_le_of_pos

added theorem Right.one_lt_mul_of_lt_of_lt

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_of_nonneg_left

added theorem le_mul_of_le_mul_of_nonneg_right

added theorem le_mul_of_le_of_one_le'

added theorem le_mul_of_le_of_one_le_of_nonneg

added theorem le_mul_of_one_le_left

added theorem le_mul_of_one_le_of_le_of_nonneg

added theorem le_mul_of_one_le_right

added theorem le_of_le_mul_of_le_one_of_nonneg_left

added theorem le_of_le_mul_of_le_one_of_nonneg_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_nonneg_right

added theorem le_of_mul_le_of_one_le_of_nonneg_left

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_le_of_one_lt_of_pos

added theorem lt_mul_of_lt_mul_of_nonneg_left

added theorem lt_mul_of_lt_mul_of_nonneg_right

added theorem lt_mul_of_lt_of_one_le'

added theorem lt_mul_of_lt_of_one_le_of_nonneg

added theorem lt_mul_of_lt_of_one_lt_of_pos

added theorem lt_mul_of_one_le_of_lt_of_nonneg

added theorem lt_mul_of_one_lt_left

added theorem lt_mul_of_one_lt_of_le_of_pos

added theorem lt_mul_of_one_lt_of_lt_of_nonneg

added theorem lt_mul_of_one_lt_of_lt_of_pos

added theorem lt_mul_of_one_lt_right

added theorem lt_of_lt_mul_of_le_one_of_nonneg_left

added theorem lt_of_lt_mul_of_le_one_of_nonneg_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_of_nonneg_left

added theorem mulPosMonoRev_iff_mulPosReflectLT

added theorem mulPosMono_iff_covariant_pos

added theorem mulPosMono_iff_mulPosStrictMono

added theorem mulPosReflectLT_iff_contravariant_pos

added theorem mul_eq_mul_iff_eq_and_eq_of_pos'

added theorem mul_eq_mul_iff_eq_and_eq_of_pos

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_left

added theorem mul_le_mul_of_le_of_le

added theorem mul_le_mul_of_nonneg_left

added theorem mul_le_mul_of_nonneg_right

added theorem mul_le_mul_right

added theorem mul_le_of_le_of_le_one'

added theorem mul_le_of_le_of_le_one_of_nonneg

added theorem mul_le_of_le_one_left

added theorem mul_le_of_le_one_of_le'

added theorem mul_le_of_le_one_of_le_of_nonneg

added theorem mul_le_of_le_one_right

added theorem mul_le_of_mul_le_of_nonneg_left

added theorem mul_le_of_mul_le_of_nonneg_right

added theorem mul_left_cancel_iff_of_pos

added theorem mul_lt_iff_lt_one_left

added theorem mul_lt_iff_lt_one_right

added theorem mul_lt_mul_left

added theorem mul_lt_mul_of_le_of_le'

added theorem mul_lt_mul_of_le_of_lt'

added theorem mul_lt_mul_of_lt_of_lt'

added theorem mul_lt_mul_of_nonneg_of_pos

added theorem mul_lt_mul_of_pos_left

added theorem mul_lt_mul_of_pos_of_nonneg

added theorem mul_lt_mul_of_pos_of_pos

added theorem mul_lt_mul_of_pos_right

added theorem mul_lt_mul_right

added theorem mul_lt_of_le_of_lt_one'

added theorem mul_lt_of_le_of_lt_one_of_pos

added theorem mul_lt_of_le_one_of_lt'

added theorem mul_lt_of_le_one_of_lt_of_nonneg

added theorem mul_lt_of_lt_of_le_one'

added theorem mul_lt_of_lt_of_le_one_of_nonneg

added theorem mul_lt_of_lt_of_lt_one_of_pos

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_le_of_pos

added theorem mul_lt_of_lt_one_of_lt_of_pos

added theorem mul_lt_of_lt_one_right

added theorem mul_lt_of_mul_lt_of_nonneg_left

added theorem mul_lt_of_mul_lt_of_nonneg_right

added theorem mul_neg_of_neg_of_pos

added theorem mul_neg_of_pos_of_neg

added theorem mul_nonpos_of_nonneg_of_nonpos

added theorem mul_nonpos_of_nonpos_of_nonneg

added theorem mul_pos_mono_iff_mul_pos_reflect_lt

added theorem mul_pos_strict_mono_iff_mul_pos_mono_rev

added theorem mul_right_cancel_iff_of_pos

added theorem mul_self_le_mul_self

added theorem neg_iff_neg_of_mul_pos

added theorem neg_of_mul_pos_left

added theorem neg_of_mul_pos_right

added theorem posMulMonoRev_iff_mulPosMonoRev

added theorem posMulMonoRev_iff_posMulReflectLT

added theorem posMulMono_iff_covariant_pos

added theorem posMulMono_iff_mulPosMono

added theorem posMulMono_iff_posMulStrictMono

added theorem posMulReflectLT_iff_contravariant_pos

added theorem posMulReflectLT_iff_mulPosReflectLT

added theorem posMulStrictMono_iff_mulPosStrictMono

added theorem pos_and_pos_or_neg_and_neg_of_mul_pos

added theorem pos_iff_pos_of_mul_pos

added theorem pos_mul_mono_iff_pos_mul_reflect_lt

added theorem pos_mul_strict_mono_iff_pos_mul_mono_rev

added theorem pos_of_mul_pos_left

added theorem pos_of_mul_pos_right

added theorem zero_lt_mul_left

added theorem zero_lt_mul_right

Modified Mathlib/Tactic/Positivity/Basic.lean

deleted theorem mul_nonneg

deleted theorem mul_pos

modified theorem pow_bit0_nonneg

modified theorem pow_nonneg

modified theorem pow_pos

Modified test/positivity.lean