Def AlgebraicGeometry.Scheme.Pullback.openCoverOfRight

Modification history

2025-10-21 18:22

Mathlib/AlgebraicGeometry/Pullbacks.lean

chore(AlgebraicGeometry): add missing lemmas about morphism classes (#30596)

Modified AlgebraicGeometry.Scheme.Pullback.openCoverOfRight View on Github →

2023-06-29 18:35

Mathlib/AlgebraicGeometry/Pullbacks.lean

feat: port AlgebraicGeometry.Pullbacks (#5583)

Added AlgebraicGeometry.Scheme.Pullback.openCoverOfRight View on Github →