mathlib
108b9235
- chore(algebra): add `sub{_mul_action,module,semiring,ring,field,algebra}.copy` (#7220)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
5 years ago
chore(algebra): add `sub{_mul_action,module,semiring,ring,field,algebra}.copy` (#7220) We already have this for sub{monoid,group}. With this in place, we can make `coe subalgebra.range` defeq to `set.range` and similar (left for a follow-up).
Author
eric-wieser
Parents
e00d688f
Loading