Theorems · Theorem · functional analysis
real_inner_self_eq_norm_mul_norm
∀ {F : Type u_3} [inst : SeminormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x : F), inner ℝ x x = ‖x‖ * ‖x‖- Defined in
- Mathlib.Analysis.InnerProductSpace.Basic
- Cited by
- 17 results in Mathlib
- Foundations
- Depth 169 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
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 and proof · cited by 5,413
- InnerProductSpacestatement and proof · cited by 3,523
- SeminormedAddCommGroupstatement and proof · cited by 2,671
- Inner.innerstatement and proof · cited by 1,089
- RCLike.reproof · cited by 319
- inner_self_eq_norm_sq_to_Kproof · cited by 72
- inner_self_eq_norm_mul_normproof · cited by 9
Cited by17
Results whose statement or proof uses this declaration.
- InnerProductGeometry.angle_add_eq_arccos_of_inner_eq_zeroproof · cited by 8
- real_inner_self_eq_norm_sqproof · cited by 7
- InnerProductGeometry.angle_selfproof · cited by 5
- EuclideanGeometry.dist_smul_vadd_eq_distproof · cited by 4
- EuclideanGeometry.inner_pos_or_eq_of_dist_le_radiusproof · cited by 3
- Quaternion.normSq_eq_norm_mul_selfproof · cited by 3
- InnerProductGeometry.sin_angle_mul_norm_mul_normproof · cited by 2
- real_inner_smul_self_rightproof · cited by 2
- InnerProductGeometry.angle_sub_eq_angle_sub_rev_of_norm_eqproof · cited by 1
- EuclideanGeometry.dist_eq_iff_eq_smul_rotation_pi_div_two_vadd_midpointproof · cited by 1
- Orientation.abs_volumeForm_apply_of_pairwise_orthogonalproof · cited by 1