Structures · Analysis
InnerProductSpace.Core
A structure requiring that a scalar product is positive definite. Some theorems that
require these assumptions are put under section InnerProductSpace.Core.
- Defined in
- Mathlib.Analysis.InnerProductSpace.Defs
- Shape
- 2 explicit arguments · adds definite
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- Real
How is a type an instance?
Loading the hierarchy index…
Assumed by9
- InnerProductSpace.Core.inner_self_eq_zero
- InnerProductSpace.Core.toInner'
- InnerProductSpace.Core.normSq_eq_zero
- InnerProductSpace.Core.toNormedAddCommGroup
- InnerProductSpace.Core.toNormedAddCommGroupOfTopology
- InnerProductSpace.Core.inner_self_ne_zero
- InnerProductSpace.Core.toNormedSpaceOfTopology
- instCoreOfCore
- InnerProductSpace.Core.topology_eq