Commit 2023-01-12 10:27 4dced5ef

View on Github →

feat port: Algebra.Order.LatticeGroup (#934) 10b4e499f43088dd3bb7b5796184ad5216648ab1 There are a lot of failures of to_additive in this file. Probably to_additive needs to be improved

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Order/LatticeGroup.lean

added theorem LatticeOrderedCommGroup.abs_abs_div_abs_le

added theorem LatticeOrderedCommGroup.abs_div_sup_mul_abs_div_inf

added theorem LatticeOrderedCommGroup.abs_inv_comm

added theorem LatticeOrderedCommGroup.inf_eq_div_pos_div

added theorem LatticeOrderedCommGroup.inf_sq_eq_mul_div_abs_div

added theorem LatticeOrderedCommGroup.inv_le_abs

added theorem LatticeOrderedCommGroup.inv_le_neg

added def LatticeOrderedCommGroup.latticeOrderedCommGroupToDistribLattice

added theorem LatticeOrderedCommGroup.le_mabs

added theorem LatticeOrderedCommGroup.m_Birkhoff_inequalities

added theorem LatticeOrderedCommGroup.m_le_iff_pos_le_neg_ge

added theorem LatticeOrderedCommGroup.m_le_pos

added theorem LatticeOrderedCommGroup.m_neg_abs

added theorem LatticeOrderedCommGroup.m_neg_part_def

added theorem LatticeOrderedCommGroup.m_pos_abs

added theorem LatticeOrderedCommGroup.m_pos_part_def

added theorem LatticeOrderedCommGroup.mabs_inf_div_inf_le_mabs

added theorem LatticeOrderedCommGroup.mabs_mabs

added theorem LatticeOrderedCommGroup.mabs_mul_le

added theorem LatticeOrderedCommGroup.mabs_of_one_le

added theorem LatticeOrderedCommGroup.mabs_sup_div_sup_le_mabs

added theorem LatticeOrderedCommGroup.mul_inf_eq_mul_inf_mul

added theorem LatticeOrderedCommGroup.neg_eq_inv_inf_one

added theorem LatticeOrderedCommGroup.neg_eq_one_iff'

added theorem LatticeOrderedCommGroup.neg_eq_one_iff

added theorem LatticeOrderedCommGroup.neg_eq_pos_inv

added theorem LatticeOrderedCommGroup.neg_le_one_iff

added theorem LatticeOrderedCommGroup.neg_of_inv_le_one

added theorem LatticeOrderedCommGroup.neg_of_le_one

added theorem LatticeOrderedCommGroup.neg_of_one_le

added theorem LatticeOrderedCommGroup.neg_of_one_le_inv

added theorem LatticeOrderedCommGroup.neg_one

added theorem LatticeOrderedCommGroup.one_le_abs

added theorem LatticeOrderedCommGroup.one_le_neg

added theorem LatticeOrderedCommGroup.one_le_pos

added theorem LatticeOrderedCommGroup.pos_div_neg

added theorem LatticeOrderedCommGroup.pos_eq_neg_inv

added theorem LatticeOrderedCommGroup.pos_eq_one_iff

added theorem LatticeOrderedCommGroup.pos_eq_self_of_one_lt_pos

added theorem LatticeOrderedCommGroup.pos_inf_neg_eq_one

added theorem LatticeOrderedCommGroup.pos_le_one_iff

added theorem LatticeOrderedCommGroup.pos_mul_neg

added theorem LatticeOrderedCommGroup.pos_of_le_one

added theorem LatticeOrderedCommGroup.pos_of_one_le

added theorem LatticeOrderedCommGroup.pos_one

added theorem LatticeOrderedCommGroup.sup_div_inf_eq_abs_div

added theorem LatticeOrderedCommGroup.sup_eq_mul_pos_div

added theorem LatticeOrderedCommGroup.sup_sq_eq_mul_mul_abs_div

added theorem inf_mul_sup

added theorem inv_inf_eq_sup_inv

added theorem inv_sup_eq_inv_inf_inv

added theorem mul_inf

added theorem mul_sup