mathlib
2e1d8d67 - feat(ring_theory/roots_of_unity): `fun_like` support (#11735)

Commit
3 years ago
feat(ring_theory/roots_of_unity): `fun_like` support (#11735) - feat(ring_theory/roots_of_unity): ring_hom_class - oops these could've been monoid homs from the start
Author
Parents
Loading