Commit 2023-11-15 13:53 9772ef6b

View on Github →

feat: Monovariance under algebraic operations (#7648) Prove a bunch of results relating monovary to algebraic operations in ordered groups.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Order/Group/Defs.lean

added theorem lt_or_lt_of_div_lt_div

Created Mathlib/Algebra/Order/Monovary.lean

added theorem Antivary.div_left

added theorem Antivary.div_left₀

added theorem Antivary.div_right

added theorem Antivary.div_right₀

added theorem Antivary.mul_left

added theorem Antivary.mul_left₀

added theorem Antivary.mul_right

added theorem Antivary.mul_right₀

added theorem Antivary.pow_left

added theorem Antivary.pow_left₀

added theorem Antivary.pow_right

added theorem Antivary.pow_right₀

added theorem AntivaryOn.div_left

added theorem AntivaryOn.div_left₀

added theorem AntivaryOn.div_right

added theorem AntivaryOn.div_right₀

added theorem AntivaryOn.mul_left

added theorem AntivaryOn.mul_left₀

added theorem AntivaryOn.mul_right

added theorem AntivaryOn.mul_right₀

added theorem AntivaryOn.pow_left

added theorem AntivaryOn.pow_left₀

added theorem AntivaryOn.pow_right

added theorem AntivaryOn.pow_right₀

added theorem Monovary.div_left

added theorem Monovary.div_left₀

added theorem Monovary.div_right

added theorem Monovary.div_right₀

added theorem Monovary.mul_left

added theorem Monovary.mul_left₀

added theorem Monovary.mul_right

added theorem Monovary.mul_right₀

added theorem Monovary.pow_left

added theorem Monovary.pow_left₀

added theorem Monovary.pow_right

added theorem Monovary.pow_right₀

added theorem MonovaryOn.div_left

added theorem MonovaryOn.div_left₀

added theorem MonovaryOn.div_right

added theorem MonovaryOn.div_right₀

added theorem MonovaryOn.mul_left

added theorem MonovaryOn.mul_left₀

added theorem MonovaryOn.mul_right

added theorem MonovaryOn.mul_right₀

added theorem MonovaryOn.pow_left

added theorem MonovaryOn.pow_left₀

added theorem MonovaryOn.pow_right

added theorem MonovaryOn.pow_right₀

added theorem antivaryOn_iff_forall_mul_nonpos

added theorem antivaryOn_iff_forall_smul_nonpos

added theorem antivaryOn_iff_mul_rearrangement

added theorem antivaryOn_iff_smul_rearrangement

added theorem antivaryOn_inv

added theorem antivaryOn_inv_left

added theorem antivaryOn_inv_left₀

added theorem antivaryOn_inv_right

added theorem antivaryOn_inv_right₀

added theorem antivaryOn_inv₀

added theorem antivary_iff_forall_mul_nonpos

added theorem antivary_iff_forall_smul_nonpos

added theorem antivary_iff_mul_rearrangement

added theorem antivary_iff_smul_rearrangement

added theorem antivary_inv

added theorem antivary_inv_left

added theorem antivary_inv_left₀

added theorem antivary_inv_right

added theorem antivary_inv_right₀

added theorem antivary_inv₀

added theorem monovaryOn_iff_forall_mul_nonneg

added theorem monovaryOn_iff_forall_smul_nonneg

added theorem monovaryOn_iff_mul_rearrangement

added theorem monovaryOn_iff_smul_rearrangement

added theorem monovaryOn_inv

added theorem monovaryOn_inv_left

added theorem monovaryOn_inv_left₀

added theorem monovaryOn_inv_right

added theorem monovaryOn_inv_right₀

added theorem monovaryOn_inv₀

added theorem monovary_iff_forall_mul_nonneg

added theorem monovary_iff_forall_smul_nonneg

added theorem monovary_iff_mul_rearrangement

added theorem monovary_iff_smul_rearrangement

added theorem monovary_inv

added theorem monovary_inv_left

added theorem monovary_inv_left₀

added theorem monovary_inv_right

added theorem monovary_inv_right₀

added theorem monovary_inv₀