mathlib
a7ec6336
- chore(algebra/*): add missing lemmas about `copy` on subobjects (#9624)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
4 years ago
chore(algebra/*): add missing lemmas about `copy` on subobjects (#9624) This adds `coe_copy` and `copy_eq` to `sub{mul_action,group,ring,semiring,field,module,algebra,lie_module}`, to match the lemmas already present on `submonoid`.
Author
eric-wieser
Parents
577cac15
Loading