Commit 2025-03-24 15:02 f3baa493

View on Github →

chore: improvements to (Mv)Polynomial and Algebra.IsPushout APIs (#23096)

Introduce better simp lemma toFunBilinear_apply_eq_smul to replace toFunBilinear_apply_apply. Closes #20332.
(Mv)Polynomial.map_in/surjective_iff: R → S is in/surjective iff the induced R[X] → S[X] is in/surjective.
Move algebraMvPolynomial from MvPolynomial/Basic.lean to MvPolynomial/Eval.lean. Saves 39 transitive imports from MvPolynomial/Localization.lean.
Golf the proof of Algebra.IsPushout.symm.
Protect Subalgebra.IsAlgebraic.

Estimated changes

Modified Mathlib/Algebra/MvPolynomial/Eval.lean

added theorem MvPolynomial.algebraMap_def

added theorem MvPolynomial.map_injective_iff

added theorem MvPolynomial.map_surjective_iff

Modified Mathlib/Algebra/Polynomial/Eval/Coeff.lean

added theorem Polynomial.map_injective_iff

added theorem Polynomial.map_surjective_iff

Modified Mathlib/RingTheory/Algebraic/Defs.lean

deleted def Subalgebra.IsAlgebraic

Modified Mathlib/RingTheory/IsTensorProduct.lean

modified theorem Algebra.IsPushout.comp_iff

modified theorem Algebra.IsPushout.symm

Modified Mathlib/RingTheory/Localization/Algebra.lean

Modified Mathlib/RingTheory/MvPolynomial/Basic.lean

deleted theorem MvPolynomial.algebraMap_def

Modified Mathlib/RingTheory/MvPolynomial/Localization.lean

Modified Mathlib/RingTheory/PolynomialAlgebra.lean

added theorem PolyEquivTensor.toFunAlgHom_apply_tmul_eq_smul

added theorem PolyEquivTensor.toFunBilinear_apply_apply

added theorem PolyEquivTensor.toFunBilinear_apply_eq_smul

added theorem Polynomial.algebraMap_def

added theorem polyEquivTensor_symm_apply_tmul_eq_smul

Modified Mathlib/RingTheory/RingHom/Locally.lean

Modified Mathlib/RingTheory/TensorProduct/MvPolynomial.lean