Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-02-25 19:22 06c55940

View on Github →

chore(analyis/normed_space/banach): split proof to avoid timeout (#2053)

  • chore(analyis/normed_space/banach): split proof to avoid timeout
  • delay introducing unnecessary variable
  • Apply suggestions from code review Co-Authored-By: sgouezel sebastien.gouezel@univ-rennes1.fr
  • fix indent

Estimated changes