Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-30 02:06 f254c2f8

View on Github →

refactor(analysis/normed_space/{dual, pi_Lp}): split out inner product space parts (#9388) This is just moving code, no math changes. https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/New.20folder.20analysis.2Finner_product_space

Estimated changes