mathlib

b7b371e1 - doc(field_theory/finite/trace): fix module docstring (#14711)

doc(field_theory/finite/trace): fix module docstring (#14711) This PR just fixes the docstring in `field_theory/finite/trace.lean`. It was still mentioning a definition that was removed.