Commit 2025-07-12 17:03 ff4b239b
View on Github →chore: generalise syntactically Over.tensorHom_left_fst (#27034)
Previously, the LHS was (f ⊗ₘ g).left ≫ pullback.fst S.hom U.hom. Now it is f ⊗ₘ g).left ≫ pullback.fst fS fU, which is syntactically more general.
From Toric