Theorem AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app

Modification history

2026-08-30 10:33
Mathlib/AlgebraicGeometry/Modules/Tilde.lean
chore: remove `CommRingCat.of` in AlgebraicGeometry\Modules\Tilde.lean (#42694) …
Modified AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_appView on Github →
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 →