Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-18 19:27 a10bc3d3

View on Github →

feat(normed_space/inner_product): euclidean_space.norm_eq (#6744)

Estimated changes

Modified src/analysis/normed_space/inner_product.lean

added theorem euclidean_space.norm_eq

added theorem pi_Lp.norm_eq_of_L2

Modified src/topology/metric_space/pi_Lp.lean

added theorem pi_Lp.norm_eq_of_nat