Mathlib Map

Theorems · Definition · commutative algebra

MvPolynomial.rename

{σ : Type u_1} →
  {τ : Type u_2} → {R : Type u_4} → [inst : CommSemiring R] → (σ → τ) → MvPolynomial σ R →ₐ[R] MvPolynomial τ R

Rename all the variables in a multivariable polynomial.

Defined in
Mathlib.Algebra.MvPolynomial.Rename
Cited by
168 results in Mathlib
Foundations
Depth 86 from the axioms, rests on 1,779 definitions · uses propext, Classical.choice, Quot.sound
Assumes
CommSemiring
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Algebra.Generators.comp · cited by 52Generators.compMvPolynomial.rename_X · cited by 48MvPolynomial.rename_XMvPolynomial.optionEquivLeft · cited by 36MvPolynomial.optionEquivL…MvPolynomial.renameEquiv · cited by 22MvPolynomial.renameEquivMvPolynomial.IsSymmetric · cited by 18MvPolynomial.IsSymmetricmap_wittStructureInt · cited by 13map_wittStructureIntMvPolynomial.rename_rename · cited by 13MvPolynomial.rename_renamewittStructureRat · cited by 12wittStructureRatMvPolynomial.renameEquiv_apply · cited by 11MvPolynomial.renameEquiv_…MvPolynomial.rename_injective · cited by 11MvPolynomial.rename_injec…MvPolynomial.aeval_rename · cited by 9MvPolynomial.aeval_renameAlgebraicIndependent.comp · cited by 9AlgebraicIndependent.compMvPolynomial.rename_id · cited by 9MvPolynomial.rename_idMvPolynomial.map_rename · cited by 8MvPolynomial.map_renameWittVector.polyOfInterest · cited by 8WittVector.polyOfInterestCommSemiring · cited by 10911CommSemiringFinsupp · cited by 5255FinsuppAlgHom · cited by 3236AlgHomMvPolynomial · cited by 2140MvPolynomialFinsupp.mapDomain.addMonoidHom · cited by 19mapDomain.addMonoidHomAddMonoidAlgebra.mapDomainAlgHom · cited by 13AddMonoidAlgebra.mapDomai…MvPolynomial.renameCITED BYCITES

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by185

Results whose statement or proof uses this declaration.