Commit 2025-12-02 04:52 84601a70

View on Github →

chore(RingTheory/LocalRing): fix problematic instance (#27445) We shouldn't use RingHom.toAlgebra for Algebra (ResidueField R) (ResidueField S). The smul should come from the smul field in Algebra.

  • Redefined Algebra (ResidueField R) (ResidueField S) via Ideal.Quotient.algebraOfLiesOver, and provided missing IsScalarTower instances for it.
  • Added missing IsScalarTower for Localization.AtPrime.
  • Removed Algebra p.ResidueField q.ResidueField and the IsScalarTower instances coming with it (because they are inferInstance now)

Estimated changes