Theorems · Theorem · functional analysis
inner_eq_norm_mul_iff_div
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
{x y : E}, x ≠ 0 → (inner 𝕜 x y = ↑‖x‖ * ↑‖y‖ ↔ (↑‖y‖ / ↑‖x‖) • x = y)- Defined in
- Mathlib.Analysis.InnerProductSpace.Basic
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 172 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites30
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Realproof · cited by 25,697
- NormedAddCommGroupstatement and proof · cited by 15,752
- Norm.normstatement and proof · cited by 5,413
- Algebra.algebraMapproof · cited by 4,706
- mul_oneproof · cited by 3,885
- InnerProductSpacestatement and proof · cited by 3,523
- one_mulproof · cited by 2,841
- RCLikestatement and proof · cited by 2,829
- Submodule.spanproof · cited by 1,504
- map_mulproof · cited by 1,137
- Inner.innerstatement and proof · cited by 1,089
Cited by2
Results whose statement or proof uses this declaration.
- real_inner_div_norm_mul_norm_eq_one_iffproof · cited by 2
- inner_eq_norm_mul_iffproof · cited by 2