Commit 2024-05-23 12:15 9c69797c

fix: make HeightOneSpectrum.adicCompletion an abbrev (#13020) IsDedekindDomain.HeightOneSpectrum.adicCompletion is currently a def and this causes a bunch of rws to fail in Lean 4; erw is needed. In developing the API further I ran into more irritating erw issues; changing it to an abbrev seems to solve them (we can get rid of several porting notes too).