Paul Lezeau

A few variables could be made implicit in some of the lemmas in `ring_theory/chain_of_divisors`. I also made a (very) minor stylistic change to a proof from one of my previous...

feat(ring_theory/dedekind_domain/ideal): the prime factorizations of `r` and `span {r}` are essentially the same in a PID

1

A definition plus some extra lemmas about PIDs that will be used in #15000 --- [](https://gitpod.io/from-referrer/)

In this PR we define the conductor ideal and prove some basic results about it. In a later PR (#16870), these will be used to prove the Dedekind-Kummer theorem in...

In this PR, we finish the proof of the general case of the Dedekind-Kummer theorem as stated in Neukirch, completing the work done in #15000. --- [](https://gitpod.io/from-referrer/)

chore: add docstring to `Simp.Methods.discharge?`

1

This PR adds a small docstring to `Simp.Methods.discharge?` - (this is what I *think* it does, so any corrections are appreciated:)) This was suggested in the review of [this mathlib...

feat(Analysis/Calculus/FwdFDerivRestrict): Add `simproc` for domain restriction with `fwdFDeriv`

3

This PR adds a simproc for restricting the domain when computing `fwdFDeriv`. Co-authored-by: Tomáš Skřivan [[email protected]](mailto:[email protected]).