Theorem UniqueFactorizationMonoid.of_existsUnique_irreducible_factors

Modification history