Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-05 13:27 6bad4c61

View on Github →

feat(ring_theory/trace): the composition of traces is trace (#8078) A little group of lemmas from the Dedekind domain project.

Estimated changes

Modified src/ring_theory/trace.lean

added theorem algebra.trace_apply

added theorem algebra.trace_comp_trace

added theorem algebra.trace_comp_trace_of_basis

added theorem algebra.trace_trace

added theorem algebra.trace_trace_of_basis