Theorem AddMonoidHom.map_trace

Modification history

2024-10-14 12:17
Mathlib/LinearAlgebra/Matrix/Trace.lean
feat: add `RingTheory.Trace.Quotient`: relations between trace maps and quotients (#14798) …
Modified AddMonoidHom.map_traceView on Github →
2023-08-11 23:48
Mathlib/LinearAlgebra/Matrix/Trace.lean
feat: add Algebra.discr_localizationLocalization (#6422) …
Added AddMonoidHom.map_traceView on Github →