Theorem spectrum.hasFPowerSeriesOnBall_inverse_one_sub_smul

Modification history

2024-09-24 06:06

Mathlib/Analysis/Normed/Algebra/Spectrum.lean

feat: define `HasSummableGeomSeries` to unify results between normed field and complete normed algebras (#17002) …

Modified spectrum.hasFPowerSeriesOnBall_inverse_one_sub_smul View on Github →

2023-06-11 13:19

Mathlib/Analysis/NormedSpace/Spectrum.lean

feat: port Analysis.NormedSpace.Spectrum (#4946)

Added spectrum.hasFPowerSeriesOnBall_inverse_one_sub_smul View on Github →