Commit 2022-03-17 22:40 a26dfc4c

feat(analysis/normed_space/basic): add normed_division_ring (#12132) This defines normed division rings and generalizes some of the lemmas that applied to normed fields instead to normed division rings. This breaks one ac_refl; although this could be resolved by using simp only {canonize_instances := tt} first, it's easier to just tweak the proof.