mathlib

51e12c00 - chore(ring_theory/fractional_ideal): change exists_eq_span_singleton_mul (#4800)

chore(ring_theory/fractional_ideal): change exists_eq_span_singleton_mul (#4800) Replace assumption `(a : K)` with `(a : R)` Add result `a \ne 0` Change `span_singleton` a to `span singleton (g.to_map a)^-1` .. in the statement of lemma `exists_eq_span_singleton_mul` Adapt dependences Co-authored-by: faenuccio <65080144+faenuccio@users.noreply.github.com>