Commit 2025-01-13 10:02 bc14fcf5

View on Github →

feat: the localization of R[X] at S is the polynomial ring over the localization of R at S (#20070) From GrowthInGroups (LeanCamCombi)

Estimated changes

Modified Mathlib/RingTheory/Localization/Algebra.lean

added theorem Polynomial.isLocalization

Modified Mathlib/RingTheory/MvPolynomial/Localization.lean

Modified Mathlib/RingTheory/PolynomialAlgebra.lean

added theorem coe_polyEquivTensor'

added theorem coe_polyEquivTensor'_symm

added def polyEquivTensor'