mathlib3
92263c0b - refactor(algebraic_geometry/structure_sheaf): Enclose definitions in structure_sheaf namespace (#8010)

Commit

4 years ago

refactor(algebraic_geometry/structure_sheaf): Enclose definitions in structure_sheaf namespace (#8010) Moves some pretty generic names like `const` and `to_open` to the `structure_sheaf` namespace.

Author

justus-springer

Parents

5bc18a9e

mathlib3 92263c0b - refactor(algebraic_geometry/structure_sheaf): Enclose definitions in structure_sheaf namespace (#8010)

mathlib3
92263c0b - refactor(algebraic_geometry/structure_sheaf): Enclose definitions in structure_sheaf namespace (#8010)