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]`.







leanprover-community/mathlib,leanprover-community/mathlib