Commit 2023-06-08 17:23 34e6b3d1

View on Github →

feat: port RingTheory.DedekindDomain.PID (#4855)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/DedekindDomain/PID.lean

added theorem FractionalIdeal.isPrincipal.of_finite_maximals_of_inv

added theorem FractionalIdeal.isPrincipal_of_unit_of_comap_mul_span_singleton_eq_top

added theorem Ideal.IsPrincipal.of_finite_maximals_of_isUnit

added theorem Ideal.eq_span_singleton_of_mem_of_not_mem_sq_of_not_mem_prime_ne

added theorem IsDedekindDomain.isPrincipalIdealRing_localization_over_prime

added theorem IsLocalization.OverPrime.mem_normalizedFactors_of_isPrime

added theorem IsPrincipalIdealRing.of_finite_primes