Theorem CategoryTheory.Projective.factorThru_comp

Modification history