Commit dfd0bdc

committed

chore: redefine LocalizedModule.

1 parent 855ce5c commit dfd0bdcCopy full SHA for dfd0bdc

6 files changed

Mathlib
- AlgebraicGeometry/Modules
  - Tilde.lean
- Algebra/Module/LocalizedModule
  - Basic.lean
- GroupTheory/OreLocalization
  - Basic.lean
  - OreSet.lean
- RingTheory
  - OreLocalization
    - Ring.lean
  - TensorProduct
    - Nontrivial.lean

Comments

(0)