mathlib3

3f777613 - feat(ring_theory/algebraic): algebraic functions (#11156)

feat(ring_theory/algebraic): algebraic functions (#11156) Accessible via a new `algebra (polynomial R) (R → R)` and a generalization that gives `algebra (polynomial R) (S → S)` when `[algebra R S]`.