Commit 2026-08-30 10:33 29bc345b

View on Github →

chore: remove CommRingCat.of in AlgebraicGeometry\Modules\Tilde.lean (#42694) A number of the definitions in AlgebraicGeometry\Modules\Tilde.lean currently have CommRingCat.of R even though R is already of type CommRingCat. This PR removes these.

Estimated changes

Modified Mathlib/AlgebraicGeometry/Modules/Tilde.lean

modified theorem AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app

modified def AlgebraicGeometry.moduleSpecΓFunctor