Theorem UniqueFactorizationMonoid.of_exists_unique_irreducible_factors

Modification history