mathlib
6bad4c61 - feat(ring_theory/trace): the composition of `trace`s is `trace` (#8078)

Commit

4 years ago

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

Author

Vierkantor

Parents