Theorem MvPolynomial.IsHomogeneous.map

Modification history

2026-04-07 10:49
Mathlib/RingTheory/MvPolynomial/Homogeneous.lean
refactor(Algebra/MvPolynomial): redefine `map` in terms of `AddMonoidAlgebra` (#37210) …
Deleted MvPolynomial.IsHomogeneous.mapView on Github →
2024-02-14 22:15
Mathlib/RingTheory/MvPolynomial/Homogeneous.lean
chore(RingTheory/MvPolynomial/Homogeneous): misc lemmas on homogeneous polyomials (#10478)
Added MvPolynomial.IsHomogeneous.mapView on Github →