Skip to content
Detect changes to header SHAs

[Merged by Bors] - feat: port AlgebraicGeometry.Morphisms.QuasiSeparated #15124

Sign in to view logs

[Merged by Bors] - feat: port AlgebraicGeometry.Morphisms.QuasiSeparated

[Merged by Bors] - feat: port AlgebraicGeometry.Morphisms.QuasiSeparated #15124

Triggered via pull request July 4, 2023 17:31
@jjaassoonnjjaassoonn
synchronize #5691
port/AlgebraicGeometry.Morphisms.QuasiSeparated
Status Success
Total duration 51s
Artifacts –

detect_sha_changes.yml

on: pull_request
Add annotations
41s
Add annotations
Fit to window
Zoom out
Zoom in

Annotations

10 notices
Synchronization: Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean#L7
See https://leanprover-community.github.io/mathlib-port-status/file/algebraic_geometry/morphisms/quasi_compact?range=13361559d66b84f80b6d5a1c4a26aa5054766725..5dc6092d09e5e489106865241986f7f2ad28d4c8
Synchronization: Mathlib/AlgebraicGeometry/RingedSpace.lean#L7
See https://leanprover-community.github.io/mathlib-port-status/file/algebraic_geometry/ringed_space?range=d39590fc8728fbf6743249802486f8c91ffe07bc..5dc6092d09e5e489106865241986f7f2ad28d4c8
Synchronization: Mathlib/AlgebraicGeometry/Scheme.lean#L7
See https://leanprover-community.github.io/mathlib-port-status/file/algebraic_geometry/Scheme?range=06c75afebd8b612d3b20fe836424298f2387ca53..88474d1b5af6d37c2ab728b757771bced7f5194c
Synchronization: Mathlib/AlgebraicGeometry/StructureSheaf.lean#L7
See https://leanprover-community.github.io/mathlib-port-status/file/algebraic_geometry/structure_sheaf?range=d39590fc8728fbf6743249802486f8c91ffe07bc..5dc6092d09e5e489106865241986f7f2ad28d4c8
Synchronization: Mathlib/CategoryTheory/Limits/Shapes/Types.lean#L7
See https://leanprover-community.github.io/mathlib-port-status/file/category_theory/limits/shapes/types?range=70fd9563a21e7b963887c9360bd29b2393e6225a..5dc6092d09e5e489106865241986f7f2ad28d4c8
Synchronization: Mathlib/Topology/QuasiSeparated.lean#L7
See https://leanprover-community.github.io/mathlib-port-status/file/topology/quasi_separated?range=dc6c365e751e34d100e80fe6e314c3c3e0fd2988..5dc6092d09e5e489106865241986f7f2ad28d4c8
Synchronization: Mathlib/Topology/Sheaves/Forget.lean#L7
See https://leanprover-community.github.io/mathlib-port-status/file/topology/sheaves/forget?range=85d6221d32c37e68f05b2e42cde6cee658dae5e9..5dc6092d09e5e489106865241986f7f2ad28d4c8
Synchronization: Mathlib/Topology/Sheaves/LocalPredicate.lean#L7
See https://leanprover-community.github.io/mathlib-port-status/file/topology/sheaves/local_predicate?range=b8fb47c4f31648a8273c864e75f06c7b759e468c..5dc6092d09e5e489106865241986f7f2ad28d4c8
Synchronization: Mathlib/Topology/Sheaves/Presheaf.lean#L7
See https://leanprover-community.github.io/mathlib-port-status/file/topology/sheaves/presheaf?range=8a318021995877a44630c898d0b2bc376fceef3b..5dc6092d09e5e489106865241986f7f2ad28d4c8
Synchronization: Mathlib/Topology/Sheaves/PresheafOfFunctions.lean#L7
See https://leanprover-community.github.io/mathlib-port-status/file/topology/sheaves/presheaf_of_functions?range=6c31dd6563a3745bf8e0b80bdd077167583ebb8f..5dc6092d09e5e489106865241986f7f2ad28d4c8