Structures · Analysis
PreInnerProductSpace.Core
A structure requiring that a scalar product is positive semidefinite and symmetric.
- Defined in
- Mathlib.Analysis.InnerProductSpace.Defs
- Shape
- 2 explicit arguments · adds conj_inner_symm, re_inner_nonneg, add_left, smul_left
Extends1
Extended by1
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by39
- InnerProductSpace.Core.toPreInner'
- InnerProductSpace.Core.inner_conj_symm
- InnerProductSpace.Core.normSq
- InnerProductSpace.Core.inner_smul_left
- InnerProductSpace.Core.toNorm
- InnerProductSpace.Core.inner_self_nonneg
- InnerProductSpace.Core.inner_zero_left
- InnerProductSpace.Core.inner_self_im
- InnerProductSpace.Core.inner_self_of_eq_zero
- InnerProductSpace.Core.inner_smul_right
- InnerProductSpace.Core.inner_add_left
- InnerProductSpace.Core.inner_smul_ofReal_left
- InnerProductSpace.Core.inner_add_right
- InnerProductSpace.Core.norm_inner_symm
- InnerProductSpace.Core.inner_smul_ofReal_right
- InnerProductSpace.Core.inner_mul_inner_self_le
- InnerProductSpace.Core.toNormedSpace
- InnerProductSpace.Core.inner_neg_left
- InnerProductSpace.Core.inner_sub_left
- InnerProductSpace.Core.norm_eq_sqrt_re_inner
- InnerProductSpace.Core.inner_neg_right
- InnerProductSpace.Core.inner_sub_right
- InnerProductSpace.Core.re_inner_smul_ofReal_smul_self
- InnerProductSpace.Core.inner_sub_sub_self
- InnerProductSpace.Core.cauchy_schwarz_aux'
- InnerProductSpace.Core.inner_re_symm
- InnerProductSpace.Core.cauchy_schwarz_aux
- InnerProductSpace.Core.inner_self_eq_norm_mul_norm
- InnerProductSpace.Core.norm_inner_le_norm
- InnerProductSpace.Core.ofReal_normSq_eq_inner_self
- InnerProductSpace.Core.inner_add_add_self
- InnerProductSpace.Core.inner_mul_symm_re_eq_norm
- InnerProductSpace.Core.normSq_eq_zero_of_eq_zero
- InnerProductSpace.Core.inner_im_symm
- InnerProductSpace.Core.inner_self_ofReal_re
- InnerProductSpace.Core.ne_zero_of_inner_self_ne_zero
- InnerProductSpace.Core.inner_zero_right
- InnerProductSpace.Core.sqrt_normSq_eq_norm
- InnerProductSpace.Core.toSeminormedAddCommGroup