mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

Define Banach algebras

Open urkud opened this issue 5 years ago • 2 comments

  • [x] Define Banach algebras: it turns out that we already have normed_algebras;
  • [ ] Prove facts about convergence of series for Banach algebras;
  • [ ] Migrate some functions to Banach algebras:
    • [x] exp (defined but duplicates real.exp and complex.exp)
    • [ ] sin/...

urkud avatar Jan 06 '20 12:01 urkud