mathlib3

257bddff - feat(algebra/algebra/spectrum): add spectral mapping for inverses (#12219)

feat(algebra/algebra/spectrum): add spectral mapping for inverses (#12219) Given a unit `a` in an algebra `A` over a field `𝕜`, the equality `(spectrum 𝕜 a)⁻¹ = spectrum 𝕜 a⁻¹` holds.