Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-11 18:49 b48b4ff0

View on Github →

feat(analysis/normed_space/inner_product): Cauchy-Schwarz equality case and other lemmas (#4571)

Estimated changes

Modified src/analysis/normed_space/inner_product.lean

added theorem abs_inner_div_norm_mul_norm_eq_one_iff

added theorem abs_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul

added theorem abs_inner_eq_norm_iff

modified def euclidean_space

added theorem norm_add_square_eq_norm_square_add_norm_square_of_inner_eq_zero

added theorem submodule.bot_orthogonal_eq_top

added theorem submodule.eq_top_iff_orthogonal_eq_bot

added theorem submodule.is_compl_orthogonal_of_is_complete

deleted theorem submodule.is_compl_orthogonal_of_is_complete_real

added theorem submodule.top_orthogonal_eq_bot

Modified src/data/complex/is_R_or_C.lean

added theorem is_R_or_C.norm_eq_abs

Modified src/geometry/euclidean/basic.lean