Theorems · Inductive type · functional analysis
PreInnerProductSpace.Core
(𝕜 : Type u_4) → (F : Type u_5) → [inst : RCLike 𝕜] → [inst_1 : AddCommGroup F] → [Module 𝕜 F] → Type (max u_4 u_5)
A structure requiring that a scalar product is positive semidefinite and symmetric.
- Defined in
- Mathlib.Analysis.InnerProductSpace.Defs
- Cited by
- 46 results in Mathlib
- Foundations
- Depth 45 from the axioms · uses propext, Quot.sound
- Assumes
- RCLikeAddCommGroupModule
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Modulestatement · cited by 20,661
- AddCommGroupstatement · cited by 12,871
- RCLikestatement · cited by 2,829
Cited by67
Results whose statement or proof uses this declaration.
- InnerProductSpace.Core.toPreInner'statement and proof · cited by 32
- norm_inner_le_normproof · cited by 14
- InnerProductSpace.Core.inner_conj_symmstatement and proof · cited by 10
- PreInnerProductSpace.Core.toInnerstatement and proof · cited by 9
- InnerProductSpace.Core.normSqstatement and proof · cited by 8
- InnerProductSpace.Core.inner_smul_leftstatement and proof · cited by 6
- InnerProductSpace.Core.toNormstatement and proof · cited by 6
- InnerProductSpace.Core.inner_self_nonnegstatement and proof · cited by 4
- InnerProductSpace.Core.inner_add_leftstatement and proof · cited by 3
- InnerProductSpace.Core.inner_self_imstatement and proof · cited by 3
- InnerProductSpace.Core.inner_self_of_eq_zerostatement and proof · cited by 3
- InnerProductSpace.Core.inner_smul_rightstatement and proof · cited by 3