Theorem CommRingCat.isPushout_of_isPushout

Modification history

2025-02-04 06:00
Mathlib/Algebra/Category/Ring/Constructions.lean
feat(AlgebraicGeometry): integral = universally closed + affine (#19419) …
Added CommRingCat.isPushout_of_isPushoutView on Github →