Commit 2021-11-24 10:42 132833b7

View on Github →

refactor(algebra.abs): Introduce has_pos_part and has_neg_part classes (#10420) refactor(algebra.abs): Introduce has_pos_part and has_neg_part classes

Estimated changes

Modified src/algebra/abs.lean

Modified src/algebra/lattice_ordered_group.lean

added theorem lattice_ordered_comm_group.m_neg_part_def

added theorem lattice_ordered_comm_group.m_pos_part_def

deleted def lattice_ordered_comm_group.mneg

deleted def lattice_ordered_comm_group.mpos

modified theorem lattice_ordered_comm_group.neg_eq_pos_inv