mathlib3
2b87435a - feat(ring_theory/trace): remove a useless assumption (#10138)

Commit

4 years ago

feat(ring_theory/trace): remove a useless assumption (#10138) We remove an assumption that is always true.

Author

riccardobrasca

Parents