Commit 2026-04-23 09:36 3325a31d

View on Github →

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

Summary

Generalizes MvPolynomial.pUnitAlgEquiv from PUnit to any uniquely inhabited index type as MvPolynomial.uniqueAlgEquiv. The old pUnitAlgEquiv API is kept as deprecated compatibility aliases, and downstream uses are migrated where appropriate. This PR adds proofs autoformalised by @Aristotle-Harmonic.

Motivation

The equivalence MvPolynomial σ R ≃ₐ[R] R[X] only needs [Unique σ], not the specific index type PUnit.

Estimated changes

Modified Mathlib/Algebra/MvPolynomial/Equiv.lean

added theorem MvPolynomial.eval₂_const_uniqueAlgEquiv

added theorem MvPolynomial.eval₂_const_uniqueAlgEquiv_symm

added theorem MvPolynomial.eval₂_uniqueAlgEquiv

added theorem MvPolynomial.eval₂_uniqueAlgEquiv_symm

modified theorem MvPolynomial.mapAlgEquiv_apply

modified theorem MvPolynomial.mapEquiv_apply

deleted def MvPolynomial.pUnitAlgEquiv

added def MvPolynomial.uniqueAlgEquiv

added theorem MvPolynomial.uniqueAlgEquiv_monomial

added theorem MvPolynomial.uniqueAlgEquiv_symm_monomial

Modified Mathlib/AlgebraicGeometry/AffineSpace.lean

Modified Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean

Modified Mathlib/RingTheory/AlgebraicIndependent/Transcendental.lean

Modified Mathlib/RingTheory/FinitePresentation.lean

Modified Mathlib/RingTheory/FreeCommRing.lean

Modified Mathlib/RingTheory/PowerSeries/Basic.lean

Modified Mathlib/RingTheory/PowerSeries/Evaluation.lean

Modified Mathlib/RingTheory/Smooth/Basic.lean