mathlib
93419b38 - chore(data/equiv/algebra): add `ring.to_mul/add_equiv`, DRY (#1247)

Commit
6 years ago
chore(data/equiv/algebra): add `ring.to_mul/add_equiv`, DRY (#1247)
Author
Committer
Parents
Loading