Theorem ModuleCat.Tilde.isLocallyFraction_pred

Modification history

2026-02-10 19:14

Mathlib/AlgebraicGeometry/Modules/Tilde.lean

chore(AlgebraicGeometry): refactor `structureSheaf` (#35090) …

Deleted ModuleCat.Tilde.isLocallyFraction_pred View on Github →

2024-07-12 13:34

Mathlib/AlgebraicGeometry/Modules/Tilde.lean

feat(AlgebraicGeometry/Modules/Tilde): construct the tilde sheaf associated to a module (#14231) …

Added ModuleCat.Tilde.isLocallyFraction_pred View on Github →