TheoremsisPrincipalIdealRing, to_principal_ideal_domain, of_comap, exists_maximal_not_isPrincipal, nonPrincipals_eq_empty_iff, nonPrincipals_zorn, span_singleton_generator, coprime_iff_not_dvd, coprime_pow_of_not_dvd, dvd_iff_not_isCoprime, isCoprime_or_dvd, associated_gcd_gcd, dvd_gcd, gcd_dvd_left, gcd_dvd_right, gcd_eq_sum, isPrincipal_of_FG, nonemptyGCDMonoid, of_isPrincipalIdealRing, span_gcd, span_gcd_eq_span_gcd, span_pair_isPrincipal, isPrincipalIdealRing, to_maximal_ideal, of_isNoetherianRing_of_isBezout, of_surjective, isCoprime, coprime_iff_not_dvd, factors_spec, isMaximal_of_irreducible, isNoetherianRing, mem_submonoid_of_factors_subset_of_units_subset, ne_zero_of_mem_factors, ringHom_mem_submonoid_of_factors_subset_of_units_subset, to_uniqueFactorizationMonoid, associated_generator_span_self, dvd_generator_span_iff, eq_bot_iff_generator_eq_zero, fg, generator_map_dvd_of_mem, generator_mem, generator_submoduleImage_dvd_of_mem, map, map_ringHom, mem_iff_eq_smul_generator, mem_iff_generator_dvd, of_comap, prime_generator_of_isPrime, bot_isPrincipal, dvd_or_isCoprime, exists_associated_pow_of_associated_pow_mul, exists_associated_pow_of_mul_eq_pow', exists_gcd_eq_mul_add_mul, gcd_dvd_iff_exists, gcd_isUnit_iff, isCoprime_of_dvd, isCoprime_of_irreducible_dvd, isCoprime_of_prime_dvd, isPrincipalIdealRing_pi_iff, isPrincipalIdealRing_prod_iff, isRelPrime_iff_isCoprime, mod_mem_iff, nonPrincipals_def, nonPrincipals_eq_empty_iff, nonPrincipals_zorn, span_gcd, span_singleton_inf_span_singleton, top_isPrincipal | 68 |