Def AlgebraicGeometry.PresheafedSpace.GlueData.ιInvAppπApp

Modification history

2023-06-23 04:14

Mathlib/AlgebraicGeometry/PresheafedSpace/Gluing.lean

feat: port AlgebraicGeometry.PresheafedSpace.Gluing (#5356)

Added AlgebraicGeometry.PresheafedSpace.GlueData.ιInvAppπApp View on Github →