Commit 2025-07-22 17:16 a38761a1
View on Github →feat(MvPolynomial/Funext): generalize (#27328) Instead of requiring the polynomials agree everywhere, it suffices to require them agree on a box with infinite sides. Live coding at Formalizing Class Field Theory, in preparation for the normal basis theorem, where the box consists of all points with coordinates in an infinite subring.