feat(ring_theory/trace): remove a useless assumption (#10138)
feat(ring_theory/trace): remove a useless assumption (#10138)

We remove an assumption that is always true.





leanprover-community/mathlib,leanprover-community/mathlib