mathlib

a26dfc4c - feat(analysis/normed_space/basic): add `normed_division_ring` (#12132)

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. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>