mathlib
6d00cc21 - feat(ring_theory/trace): Add `trace_eq_sum_automorphisms`, `norm_eq_prod_automorphisms`, `normal.alg_hom_equiv_aut` (#14523)

Commit

3 years ago

feat(ring_theory/trace): Add `trace_eq_sum_automorphisms`, `norm_eq_prod_automorphisms`, `normal.alg_hom_equiv_aut` (#14523) Co-authored-by: Iván Sadofschi Costa <isadofschi@users.noreply.github.com>

Author

isadofschi

Parents

efe794c3

mathlib 6d00cc21 - feat(ring_theory/trace): Add `trace_eq_sum_automorphisms`, `norm_eq_prod_automorphisms`, `normal.alg_hom_equiv_aut` (#14523)

mathlib
6d00cc21 - feat(ring_theory/trace): Add `trace_eq_sum_automorphisms`, `norm_eq_prod_automorphisms`, `normal.alg_hom_equiv_aut` (#14523)