Theorems · Theorem · functional analysis
parallelogram_law_with_norm_mul
∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E),
‖x + y‖ * ‖x + y‖ + ‖x - y‖ * ‖x - y‖ = 2 * (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)- Defined in
- Mathlib.Analysis.InnerProductSpace.Basic
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 164 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Realstatement and proof · cited by 25,697
- Norm.normstatement · cited by 5,413
- InnerProductSpacestatement and proof · cited by 3,523
- RCLikestatement and proof · cited by 2,829
- SeminormedAddCommGroupstatement and proof · cited by 2,671
- Inner.innerproof · cited by 1,089
- RCLike.reproof · cited by 319
- two_mulproof · cited by 232
- AddMonoidHom.map_addproof · cited by 48
- inner_self_eq_norm_mul_normproof · cited by 9
- parallelogram_lawproof · cited by 1
Cited by4
Results whose statement or proof uses this declaration.
- exists_norm_eq_iInf_of_complete_convexproof · cited by 1
- parallelogram_law_with_nnnorm_mulproof · cited by 1
- parallelogram_law_with_normproof · cited by 1
- InnerProductSpace.toInnerProductSpaceableproof · cited by 0