mathlib
8e4ef23a - refactor(*): kill int multiplication diamonds (#7255)

Commit
4 years ago
refactor(*): kill int multiplication diamonds (#7255) Insert a data field `gsmul` in `add_comm_group` containing a Z-action, and use it to make sure that all diamonds related to `Z` -actions disappear. Followup to #7084 Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Mario Carneiro <di.gama@gmail.com>
Author
Parents
Loading