Commit 2024-11-02 09:43 21d62a67

View on Github →

chore(RingTheory): Remove bad instances about Module.Flat (#18537)

Estimated changes

Modified Mathlib/RingTheory/Flat/Basic.lean

added theorem Module.Flat.of_shrink

added theorem Module.Flat.of_ulift