mathlib
cae77dc7 - feat(algebra/direct_sum): Fix two todos about generalizing over unique types (#4764)

Commit

5 years ago

feat(algebra/direct_sum): Fix two todos about generalizing over unique types (#4764) Also promotes `id` to a `≃+`, and prefers coercion over direct use of `subtype.val`.

References

#4925 - Make prime-avoidance branch build

Author

eric-wieser

Parents

de6a9d41

mathlib cae77dc7 - feat(algebra/direct_sum): Fix two todos about generalizing over unique types (#4764)

mathlib
cae77dc7 - feat(algebra/direct_sum): Fix two todos about generalizing over unique types (#4764)