mathlib3
f028ff2b - feat(algebra/hom/group_instances): add missing `int_cast` and `nat_cast` lemmas to `add_monoid.End` and `module.End` (#15839)

Commit
3 years ago
feat(algebra/hom/group_instances): add missing `int_cast` and `nat_cast` lemmas to `add_monoid.End` and `module.End` (#15839) We already had provided the `nat_cast` field for `add_monoid.End`, this just copies the same pattern to the three other fields, and adds the 8 missing `rfl` lemmas. Co-authored-by: Oliver Nash <github@olivernash.org>
Author
Parents
Loading