Theorem IsCompactOperator.antilipschitz_of_not_hasEigenvalue

Modification history

2026-03-10 18:51
Mathlib/Analysis/Normed/Operator/FredholmAlternative.lean
feat(Analysis/Normed/Operator): prove the Fredholm alternative (#35048) …
Added IsCompactOperator.antilipschitz_of_not_hasEigenvalueView on Github →