Theorem AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app

Modification history

2026-02-12 07:09
Mathlib/AlgebraicGeometry/Modules/Tilde.lean
feat(AlgebraicGeometry): tilde-Gamma adjunction (#35123)
Added AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_appView on Github →