Theorem CategoryTheory.GrothendieckTopology.MayerVietorisSquare.isPushoutAddCommGrpFreeSheaf

Modification history

2025-10-12 18:01

Mathlib/CategoryTheory/Sites/MayerVietorisSquare.lean

chore: rename `Grp` to `GrpCat` (#30191) …

Modified CategoryTheory.GrothendieckTopology.MayerVietorisSquare.isPushoutAddCommGrpFreeSheaf View on Github →

2024-08-23 21:19

Mathlib/CategoryTheory/Sites/MayerVietorisSquare.lean

feat(CategoryTheory/Sites): constructors for Mayer-Vietoris squares (#14867) …

Added CategoryTheory.GrothendieckTopology.MayerVietorisSquare.isPushoutAddCommGrpFreeSheaf View on Github →