Commit 2025-01-20 15:19 5426682c
View on Github →feat(RingTheory/Trace): the trace from a ring R to itself is the identity (#20865)
Proof that Algebra.trace R R a = a.
feat(RingTheory/Trace): the trace from a ring R to itself is the identity (#20865)
Proof that Algebra.trace R R a = a.