Commit 2025-12-02 18:14 2ad03872

View on Github →

chore: golf using simpa (#32351)

Estimated changes

Modified Mathlib/Order/Filter/Pointwise.lean

Modified Mathlib/RingTheory/Localization/Finiteness.lean

Modified Mathlib/RingTheory/Polynomial/Basic.lean

Modified Mathlib/RingTheory/RingHom/Finite.lean

Modified Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean

Modified Mathlib/Topology/VectorBundle/Basic.lean