mathlib
132833b7 - refactor(algebra.abs): Introduce `has_pos_part` and `has_neg_part` classes (#10420)

Commit

4 years ago

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

Author

mans0954

Parents

09b4bfc9

mathlib 132833b7 - refactor(algebra.abs): Introduce `has_pos_part` and `has_neg_part` classes (#10420)

mathlib
132833b7 - refactor(algebra.abs): Introduce `has_pos_part` and `has_neg_part` classes (#10420)