Theorem Algebra.trace_self_apply

Modification history

2025-01-20 15:19
Mathlib/RingTheory/Trace/Defs.lean
feat(RingTheory/Trace): the trace from a ring `R` to itself is the identity (#20865) …
Added Algebra.trace_self_applyView on Github →