Theorem Module.Flat.of_forall_exists_factorization

Modification history