Documentation Verification Report

StandardSubspace

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

Statistics

Metric	Count
Definitions `instInnerProductSpaceReal`, `mulI`, `symplComp`, `UnitI`, `StandardSubspace`, `mulI`, `symplComp`, `toClosedSubmodule`, `scalarSMulCLE`	9
Theorems `inner_real_eq_re_inner`, `involutive_mulI`, `mem_iff`, `mem_symplComp_iff`, `mulI_inf`, `mulI_mulI_eq`, `mulI_orthogonal`, `mulI_orthogonal_eq_symplComp`, `mulI_sup`, `mulI_symplComp`, `symplComp_inf`, `symplComp_sup`, `symplComp_symplComp_eq`, `val_UnitI`, `val_inv_UnitI`, `IsCyclic`, `IsSeparating`, `ext`, `ext_iff`, `involutive_symplComp`, `symplComp_symplComp_eq`, `toClosedSubmodule_inj`, `toClosedSubmodule_injective`, `scalarSMulCLE_apply`, `scalarSMulCLE_symm_apply`	25
Total	34

ClosedSubmodule

Definitions

Name	Category	Theorems
`instInnerProductSpaceReal` 📖	CompOp	10 math math: `mem_iff`, `inner_real_eq_re_inner`, `mulI_sup`, `mem_symplComp_iff`, `mulI_inf`, `symplComp_sup`, `involutive_mulI`, `symplComp_inf`, `mulI_orthogonal_eq_symplComp`, `mulI_orthogonal`
`mulI` 📖	CompOp	9 math math: `mulI_sup`, `StandardSubspace.IsSeparating`, `StandardSubspace.IsCyclic`, `mulI_inf`, `mulI_symplComp`, `mulI_mulI_eq`, `involutive_mulI`, `mulI_orthogonal_eq_symplComp`, `mulI_orthogonal`
`symplComp` 📖	CompOp	6 math math: `mem_symplComp_iff`, `mulI_symplComp`, `symplComp_sup`, `symplComp_symplComp_eq`, `symplComp_inf`, `mulI_orthogonal_eq_symplComp`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inner_real_eq_re_inner` 📖	mathematical	—	`Inner.inner` `Real` `InnerProductSpace.toInner` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `instInnerProductSpaceReal` `Complex.re` `Complex` `CStarModule.toInner` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing` `CommCStarAlgebra.toNonUnitalCommCStarAlgebra` `instCommCStarAlgebraComplex` `Complex.instStarRing` `Complex.instModuleSelf` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Complex.instNormedField` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `Complex.partialOrder` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `Complex.instNorm` `NormedAddCommGroup.toNorm` `WithCStarModule.instCStarModuleComplex`	—	—
`involutive_mulI` 📖	mathematical	—	`Function.Involutive` `ClosedSubmodule` `Real` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `instInnerProductSpaceReal` `mulI`	—	`mulI_mulI_eq`
`mem_iff` 📖	mathematical	—	`ClosedSubmodule` `Real` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `instInnerProductSpaceReal` `SetLike.instMembership` `instSetLike` `Set` `Set.instMembership` `AddSubsemigroup.carrier` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddSubmonoid.toAddSubsemigroup` `Submodule.toAddSubmonoid` `toSubmodule`	—	—
`mem_symplComp_iff` 📖	mathematical	—	`ClosedSubmodule` `Real` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Real.instRCLike` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `instInnerProductSpaceReal` `SetLike.instMembership` `instSetLike` `symplComp` `Complex.im` `Inner.inner` `Complex` `CStarModule.toInner` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing` `CommCStarAlgebra.toNonUnitalCommCStarAlgebra` `instCommCStarAlgebraComplex` `Complex.instStarRing` `Complex.instModuleSelf` `NormedAddCommGroup.toAddCommGroup` `Complex.instNormedField` `Complex.instRCLike` `Complex.partialOrder` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Module.toDistribMulAction` `Complex.instNorm` `NormedAddCommGroup.toNorm` `WithCStarModule.instCStarModuleComplex` `Real.instZero`	—	`RingHomInvPair.ids` `Units.val_inv_eq_inv_val` `Complex.inv_I` `neg_smul` `CStarModule.inner_op_smul_left` `Complex.conj_I` `mul_neg` `MulZeroClass.mul_zero` `mul_one` `zero_sub` `neg_neg` `IsScalarTower.left` `Complex.I_mul_I` `one_smul` `CStarModule.inner_neg_left` `CStarAlgebra.toStarModule` `add_zero`
`mulI_inf` 📖	mathematical	—	`mulI` `ClosedSubmodule` `Real` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `instInnerProductSpaceReal` `instInf` `NormedSpace.complexToReal` `Complex` `Complex.instRCLike`	—	`mulI.eq_1` `mapEquiv_inf_eq`
`mulI_mulI_eq` 📖	mathematical	—	`mulI`	—	`ext` `Set.ext` `RingHomInvPair.ids` `Units.val_inv_eq_inv_val` `Complex.inv_I` `neg_smul` `smul_neg` `one_smul` `neg_neg` `Units.instIsScalarTower` `IsScalarTower.left` `neg_mul` `Complex.I_mul_I` `SetLike.forall_smul_mem_iff` `instSMulMemClass` `mem_mapEquiv_iff`
`mulI_orthogonal` 📖	mathematical	—	`mulI` `orthogonal` `Real` `Real.instRCLike` `instInnerProductSpaceReal`	—	`mulI_orthogonal_eq_symplComp`
`mulI_orthogonal_eq_symplComp` 📖	mathematical	—	`mulI` `orthogonal` `Real` `Real.instRCLike` `instInnerProductSpaceReal` `symplComp`	—	`ext` `Set.ext` `mem_iff` `mem_symplComp_iff` `RingHomInvPair.ids` `mem_mapEquiv_iff` `scalarSMulCLE_symm_apply` `Units.inv_val` `Units.val_inv` `Units.smul_mk_apply` `Units.val_inv_eq_inv_val` `Complex.inv_I` `neg_smul` `inner_neg_right` `CStarModule.inner_op_smul_right` `MulZeroClass.zero_mul` `one_mul` `zero_sub` `neg_neg`
`mulI_sup` 📖	mathematical	—	`mulI` `ClosedSubmodule` `Real` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `instInnerProductSpaceReal` `instMax` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `Real.pseudoMetricSpace` `Real.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `NormedSpace.complexToReal` `Complex` `Complex.instRCLike`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `mulI.eq_1` `mapEquiv_sup_eq`
`mulI_symplComp` 📖	mathematical	—	`mulI` `symplComp`	—	`symplComp.eq_1` `mulI_orthogonal_eq_symplComp`
`symplComp_inf` 📖	mathematical	—	`symplComp` `ClosedSubmodule` `Real` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `instInnerProductSpaceReal` `instInf` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `instMax` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `Real.pseudoMetricSpace` `Real.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `symplComp.eq_1` `mulI_inf` `sup_orthogonal`
`symplComp_sup` 📖	mathematical	—	`symplComp` `ClosedSubmodule` `Real` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `instInnerProductSpaceReal` `instMax` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `Real.pseudoMetricSpace` `Real.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `instInf`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `symplComp.eq_1` `mulI_sup` `inf_orthogonal`
`symplComp_symplComp_eq` 📖	mathematical	—	`symplComp`	—	`mulI_symplComp` `mulI_mulI_eq` `orthogonal_orthogonal_eq` `Submodule.instHasOrthogonalProjectionOfCompleteSpace`

Complex

Definitions

Name	Category	Theorems
`UnitI` 📖	CompOp	2 math math: `val_UnitI`, `val_inv_UnitI`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`val_UnitI` 📖	mathematical	—	`Units.val` `Complex` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `UnitI` `I`	—	—
`val_inv_UnitI` 📖	mathematical	—	`Units.val` `Complex` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `Units` `Units.instInv` `UnitI` `instNeg` `I`	—	—

StandardSubspace

Definitions

Name	Category	Theorems
`mulI` 📖	CompOp	—
`symplComp` 📖	CompOp	2 math math: `involutive_symplComp`, `symplComp_symplComp_eq`
`toClosedSubmodule` 📖	CompOp	5 math math: `toClosedSubmodule_injective`, `toClosedSubmodule_inj`, `IsSeparating`, `IsCyclic`, `ext_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`IsCyclic` 📖	mathematical	—	`ClosedSubmodule` `Real` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `NormedSpace.complexToReal` `InnerProductSpace.toNormedSpace` `Complex` `Complex.instRCLike` `ClosedSubmodule.instMax` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `Real.pseudoMetricSpace` `Real.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `toClosedSubmodule` `ClosedSubmodule.mulI` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `ClosedSubmodule.instPartialOrder` `ClosedSubmodule.instOrderTop`	—	—
`IsSeparating` 📖	mathematical	—	`ClosedSubmodule` `Real` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `NormedSpace.complexToReal` `InnerProductSpace.toNormedSpace` `Complex` `Complex.instRCLike` `ClosedSubmodule.instInf` `toClosedSubmodule` `ClosedSubmodule.mulI` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `ClosedSubmodule.instPartialOrder` `ClosedSubmodule.instOrderBot` `T2Space.t1Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	—	—
`ext` 📖	—	`toClosedSubmodule`	—	—	`T2Space.t1Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul`
`ext_iff` 📖	mathematical	—	`toClosedSubmodule`	—	`ext`
`involutive_symplComp` 📖	mathematical	—	`Function.Involutive` `StandardSubspace` `symplComp`	—	`symplComp_symplComp_eq`
`symplComp_symplComp_eq` 📖	mathematical	—	`symplComp`	—	`ClosedSubmodule.symplComp_symplComp_eq`
`toClosedSubmodule_inj` 📖	mathematical	—	`toClosedSubmodule`	—	`ext_iff`
`toClosedSubmodule_injective` 📖	mathematical	—	`StandardSubspace` `ClosedSubmodule` `Real` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `NormedSpace.complexToReal` `InnerProductSpace.toNormedSpace` `Complex` `Complex.instRCLike` `toClosedSubmodule`	—	—

(root)

Definitions

Name	Category	Theorems
`StandardSubspace` 📖	CompData	2 math math: `StandardSubspace.toClosedSubmodule_injective`, `StandardSubspace.involutive_symplComp`
`scalarSMulCLE` 📖	CompOp	2 math math: `scalarSMulCLE_symm_apply`, `scalarSMulCLE_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`scalarSMulCLE_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearEquiv` `Real` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `NormedSpace.complexToReal` `InnerProductSpace.toNormedSpace` `Complex` `Complex.instRCLike` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike` `scalarSMulCLE` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Units.instSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Module.toDistribMulAction` `Complex.instNormedField`	—	`RingHomInvPair.ids`
`scalarSMulCLE_symm_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearEquiv` `Real` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `NormedSpace.complexToReal` `InnerProductSpace.toNormedSpace` `Complex` `Complex.instRCLike` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike` `ContinuousLinearEquiv.symm` `scalarSMulCLE` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Units.instSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Module.toDistribMulAction` `Complex.instNormedField` `Units.instInv`	—	`RingHomInvPair.ids`

---

← Back to Index