Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-22 07:22 3f9b52ae

View on Github →

refactor(ring_theory/*): make PID class a predicate (#3114)

Estimated changes

Modified src/data/zsqrtd/gaussian_int.lean

Modified src/field_theory/splitting_field.lean

Modified src/number_theory/sum_two_squares.lean

Modified src/ring_theory/adjoin_root.lean

Modified src/ring_theory/fractional_ideal.lean

Modified src/ring_theory/ideals.lean

added theorem ideal.factors_decreasing

Modified src/ring_theory/principal_ideal_domain.lean

modified theorem is_prime.to_maximal_ideal

deleted theorem principal_ideal_domain.associates_irreducible_iff_prime

deleted theorem principal_ideal_domain.factors_decreasing

deleted theorem principal_ideal_domain.factors_spec

deleted theorem principal_ideal_domain.irreducible_iff_prime

deleted theorem principal_ideal_domain.is_maximal_of_irreducible

added theorem principal_ideal_ring.associates_irreducible_iff_prime

added theorem principal_ideal_ring.factors_spec

added theorem principal_ideal_ring.irreducible_iff_prime

added theorem principal_ideal_ring.is_maximal_of_irreducible