Commit 2023-03-21 11:38 9d04f3cc

View on Github →

feat: port RingTheory.PrincipalIdealDomain (#3012)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/PrincipalIdealDomain.lean

added theorem Ideal.IsPrincipal.of_comap

added theorem Ideal.span_singleton_generator

added theorem Irreducible.coprime_iff_not_dvd

added theorem Irreducible.coprime_or_dvd

added theorem Irreducible.coprime_pow_of_not_dvd

added theorem Irreducible.dvd_iff_not_coprime

added theorem IsField.isPrincipalIdealRing

added theorem IsPrime.to_maximal_ideal

added theorem IsPrincipalIdealRing.of_prime

added theorem IsPrincipalIdealRing.of_surjective

added theorem Prime.coprime_iff_not_dvd

added theorem PrincipalIdealRing.associates_irreducible_iff_prime

added theorem PrincipalIdealRing.factors_spec

added theorem PrincipalIdealRing.irreducible_iff_prime

added theorem PrincipalIdealRing.isMaximal_of_irreducible

added theorem PrincipalIdealRing.mem_submonoid_of_factors_subset_of_units_subset

added theorem PrincipalIdealRing.ne_zero_of_mem_factors

added theorem PrincipalIdealRing.ringHom_mem_submonoid_of_factors_subset_of_units_subset

added theorem Submodule.IsPrincipal.eq_bot_iff_generator_eq_zero

added theorem Submodule.IsPrincipal.generator_map_dvd_of_mem

added theorem Submodule.IsPrincipal.generator_mem

added theorem Submodule.IsPrincipal.generator_submoduleImage_dvd_of_mem

added theorem Submodule.IsPrincipal.mem_iff_eq_smul_generator

added theorem Submodule.IsPrincipal.mem_iff_generator_dvd

added theorem Submodule.IsPrincipal.of_comap

added theorem Submodule.IsPrincipal.prime_generator_of_isPrime

added theorem Submodule.IsPrincipal.principal

added theorem Submodule.IsPrincipal.span_singleton_generator

added theorem dvd_or_coprime

added theorem exists_associated_pow_of_mul_eq_pow'

added theorem exists_gcd_eq_mul_add_mul

added theorem gcd_dvd_iff_exists

added theorem gcd_isUnit_iff

added theorem isCoprime_of_dvd

added theorem isCoprime_of_irreducible_dvd

added theorem isCoprime_of_prime_dvd

added theorem mod_mem_iff

added def nonPrincipals

added theorem nonPrincipals_def

added theorem nonPrincipals_eq_empty_iff

added theorem nonPrincipals_zorn

added theorem span_gcd