Commit 2024-07-30 13:16 48bbda47

View on Github →

feat(Algebra/Category/Ring): Add dsimp lemmas for CommRingCat. (#15297)

Estimated changes

Modified Mathlib/Algebra/Category/Ring/Basic.lean

added theorem CommRingCat.comp_apply

added theorem CommRingCat.forget_obj

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean

Modified Mathlib/AlgebraicGeometry/Spec.lean