mathlib3

aafeb5f3 - feat(ring_theory/dedekind_domain): promote fractional ideals to `semifield` (#15794)

feat(ring_theory/dedekind_domain): promote fractional ideals to `semifield` (#15794) This is the first nontrivial semifield instance in mathlib! We can just upgrade the existing `comm_group_with_zero` instance to `semifield`. cc @YaelDillies