Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-06 12:25 74373b81

View on Github →

feat(algebra/lattice_ordered_group): add basic theory of lattice ordered groups (#8673)

Estimated changes

Modified docs/references.bib

Modified src/algebra/field_power.lean

Modified src/algebra/group/basic.lean

added theorem div_mul_comm

Created src/algebra/lattice_ordered_group.lean

added theorem inf_mul_sup

added theorem inv_inf_eq_sup_inv

added theorem inv_sup_eq_inv_inf_inv

added theorem lattice_ordered_comm_group.abs_div_sup_mul_abs_div_inf

added theorem lattice_ordered_comm_group.inf_eq_div_pos_div

added theorem lattice_ordered_comm_group.inv_le_abs

added def lattice_ordered_comm_group.lattice_ordered_comm_group_to_distrib_lattice

added theorem lattice_ordered_comm_group.le_mabs

added theorem lattice_ordered_comm_group.m_Birkhoff_inequalities

added theorem lattice_ordered_comm_group.m_le_iff_pos_le_neg_ge

added theorem lattice_ordered_comm_group.m_le_neg

added theorem lattice_ordered_comm_group.m_le_pos

added theorem lattice_ordered_comm_group.m_neg_pos

added theorem lattice_ordered_comm_group.m_pos_pos

added theorem lattice_ordered_comm_group.m_pos_pos_id

added theorem lattice_ordered_comm_group.mabs_idempotent

added theorem lattice_ordered_comm_group.mabs_pos

added theorem lattice_ordered_comm_group.mabs_pos_eq

added theorem lattice_ordered_comm_group.mabs_triangle

added def lattice_ordered_comm_group.mneg

added def lattice_ordered_comm_group.mpos

added theorem lattice_ordered_comm_group.mul_inf_eq_mul_inf_mul

added theorem lattice_ordered_comm_group.neg_eq_inv_inf_one

added theorem lattice_ordered_comm_group.neg_eq_pos_inv

added theorem lattice_ordered_comm_group.pos_div_neg'

added theorem lattice_ordered_comm_group.pos_eq_neg_inv

added theorem lattice_ordered_comm_group.pos_inf_neg_eq_one

added theorem lattice_ordered_comm_group.pos_inv_neg

added theorem lattice_ordered_comm_group.pos_mul_neg

added theorem lattice_ordered_comm_group.sup_div_inf_eq_abs_div

added theorem lattice_ordered_comm_group.sup_eq_mul_pos_div

added theorem lattice_ordered_comm_group.sup_sq_eq_mul_mul_abs_div

added theorem lattice_ordered_comm_group.two_inf_eq_mul_div_abs_div

added theorem mul_sup_eq_mul_sup_mul

Modified src/algebra/ordered_group.lean

deleted def abs

added theorem abs_eq_max_neg

added def mabs

Modified src/algebra/ordered_ring.lean

modified theorem abs_eq_neg_self

modified theorem abs_eq_self

Modified src/data/int/cast.lean

Modified src/data/rat/cast.lean

Modified src/data/real/hyperreal.lean

modified theorem hyperreal.coe_abs

Modified src/order/filter/filter_product.lean

added theorem filter.germ.lattice_of_linear_order_eq_filter_germ_lattice

Modified src/topology/continuous_function/algebra.lean

Modified src/topology/metric_space/basic.lean