Commit 2022-02-22 15:16 f0401b91
View on Github →chore(ring_theory): split localization.lean and dedekind_domain.lean (#12206)
These files were rather long and had hundreds-deep dependency graphs. I split them into smaller files with less imports, so that they are easier to build and modify.
Proof nothing was lost:
$ cat src/ring_theory/localization/*.lean | sort | comm -23 <(sort src/ring_theory/localization.lean) - | grep -E 'lemma|theorem|def|instance|class'
$ cat src/ring_theory/dedekind_domain/*.lean | sort | comm -23 <(sort src/ring_theory/dedekind_domain.lean) - | grep -E 'lemma|theorem|def|instance|class'
giving three equivalent definitions (TODO: and shows that they are equivalent).