Theorem CategoryTheory.Over.prodComparisonIso_pullback_Spec_inv_left_fst_fst'

Modification history

2025-11-30 12:04
Mathlib/CategoryTheory/Monoidal/Cartesian/Over.lean
feat: a pullback of schemes is canonically over the second component (#31475) …
Added CategoryTheory.Over.prodComparisonIso_pullback_Spec_inv_left_fst_fst'View on Github →