Commit 2025-02-20 13:57 fb5625ce

View on Github →

feat(Algebra/MvPolynomial): add comp versions of rename lemmas (#21259) Also unapply MvPolynomial.rename_id.

Estimated changes

Modified Mathlib/Algebra/MvPolynomial/Rename.lean

added theorem MvPolynomial.aeval_comp_rename

added theorem MvPolynomial.map_comp_rename

added theorem MvPolynomial.rename_comp_rename

modified theorem MvPolynomial.rename_id

added theorem MvPolynomial.rename_id_apply

Modified Mathlib/RingTheory/MvPolynomial/Symmetric/Defs.lean