mathlib3
f0401b91 - chore(ring_theory): split `localization.lean` and `dedekind_domain.lean` (#12206)

Commit
4 years ago
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: ```bash $ 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). ``` Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Splitting.20.60localization.2Elean.60.20and.20.60dedekind_domain.2Elean
Author
Parents
Loading