Documentation Verification Report

MulOpposite

📁 Source: Mathlib/Analysis/InnerProductSpace/MulOpposite.lean

Statistics

Metric	Count
Definitions `instInner`, `instInnerProductSpace`, `mulOpposite`	3
Theorems `mulOpposite_is_orthonormal_iff`, `inner_op`, `inner_unop`, `toBasis_mulOpposite`	4
Total	7

Module.Basis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mulOpposite_is_orthonormal_iff` 📖	mathematical	—	`Orthonormal` `MulOpposite` `MulOpposite.instSeminormedAddCommGroup` `MulOpposite.instInnerProductSpace` `DFunLike.coe` `Module.Basis` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `MulOpposite.instAddCommMonoid` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `MulOpposite.instModule` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `instFunLike` `mulOpposite`	—	—

MulOpposite

Definitions

Name	Category	Theorems
`instInner` 📖	CompOp	2 math math: `inner_op`, `inner_unop`
`instInnerProductSpace` 📖	CompOp	2 math math: `Module.Basis.mulOpposite_is_orthonormal_iff`, `OrthonormalBasis.toBasis_mulOpposite`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inner_op` 📖	mathematical	—	`Inner.inner` `MulOpposite` `instInner` `op`	—	—
`inner_unop` 📖	mathematical	—	`Inner.inner` `unop` `MulOpposite` `instInner`	—	—

OrthonormalBasis

Definitions

Name	Category	Theorems
`mulOpposite` 📖	CompOp	1 math math: `toBasis_mulOpposite`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toBasis_mulOpposite` 📖	mathematical	—	`toBasis` `MulOpposite` `MulOpposite.instNormedAddCommGroup` `MulOpposite.instInnerProductSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `mulOpposite` `Module.Basis.mulOpposite` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace`	—	—

---

← Back to Index