Theorem CategoryTheory.Limits.map_ι_comp_inv_sigmaComparison

Modification history

2025-11-08 15:24

Mathlib/CategoryTheory/Limits/Preserves/Shapes/Products.lean

feat(Algebra/Category/ModuleCat/Sheaf): `O_S ⟶ f_* O_X` and `f^* O_S ≅ O_X` (#30398)

Added CategoryTheory.Limits.map_ι_comp_inv_sigmaComparison View on Github →