feat: port Data.Polynomial.AlgebraMap (#2822)

- [x] depends on: #2817
leanprover-community · Mar 13, 2023 · 6f2b42f · 6f2b42f
1 parent 0177db7
commit 6f2b42f
Show file tree

Hide file tree

Showing 2 changed files with 527 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -757,6 +757,7 @@ import Mathlib.Data.Part
 import Mathlib.Data.Pi.Algebra
 import Mathlib.Data.Pi.Interval
 import Mathlib.Data.Pi.Lex
+import Mathlib.Data.Polynomial.AlgebraMap
 import Mathlib.Data.Polynomial.Basic
 import Mathlib.Data.Polynomial.Cardinal
 import Mathlib.Data.Polynomial.Coeff