Theorem MvPolynomial.mapEquiv_apply

Modification history

2026-04-23 09:36

Mathlib/Algebra/MvPolynomial/Equiv.lean

refactor(Algebra/MvPolynomial): generalize pUnitAlgEquiv to Unique (#37801) …

Modified MvPolynomial.mapEquiv_apply View on Github →

2026-04-07 10:49

Mathlib/Algebra/MvPolynomial/Equiv.lean

refactor(Algebra/MvPolynomial): redefine `map` in terms of `AddMonoidAlgebra` (#37210) …

Added MvPolynomial.mapEquiv_apply View on Github →