Commit 2024-11-05 07:31 76ffa613

View on Github →

feat(ModelTheory): Turning polynomials into ring terms (#16503)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/MvPolynomial/FreeCommRing.lean

added theorem FirstOrder.Ring.MvPolynomialSupportLEEquiv_symm_apply_coeff

added def FirstOrder.Ring.genericPolyMap

added theorem FirstOrder.Ring.lift_genericPolyMap