Documentation Verification Report

Dual

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

Statistics

Metric	Count
Definitions `continuousLinearMapOfBilin`, `toDual`, `toDualMap`	3
Theorems `continuousLinearMapOfBilin_apply`, `continuousLinearMapOfBilin_zero`, `ext_inner_left_basis`, `ext_inner_right_basis`, `innerSL_norm`, `instIsContPerfPairRealInnerₗOfCompleteSpace`, `nullSubmodule_le_ker_toDualMap_left`, `nullSubmodule_le_ker_toDualMap_right`, `rank_rankOne`, `toContinuousLinearMap_toDualMap`, `toDualMap_apply`, `toDualMap_apply_apply`, `toDual_apply`, `toDual_apply_apply`, `toDual_apply_eq_toDualMap_apply`, `toDual_symm_apply`, `toLinearIsometry_toDual`, `unique_continuousLinearMapOfBilin`, `innerSL_inj`	19
Total	22

InnerProductSpace

Definitions

Name	Category	Theorems
`continuousLinearMapOfBilin` 📖	CompOp	8 math math: `unique_continuousLinearMapOfBilin`, `IsCoercive.range_eq_top`, `IsCoercive.bounded_below`, `continuousLinearMapOfBilin_zero`, `IsCoercive.ker_eq_bot`, `continuousLinearMapOfBilin_apply`, `IsCoercive.isClosed_range`, `IsCoercive.antilipschitz`
`toDual` 📖	CompOp	15 math math: `toLinearIsometry_toDual`, `hasFDerivAt_iff_hasGradientAt`, `toDual_symm_apply`, `MeasureTheory.charFun_toDual_symm_eq_charFunDual`, `hasGradientWithinAt_iff_hasFDerivWithinAt`, `HasFDerivWithinAt.hasGradientWithinAt`, `toDual_apply`, `toDual_apply_apply`, `ContinuousLinearMap.adjointAux_apply`, `HasGradientAt.hasFDerivAt`, `hasGradientAt_iff_hasFDerivAt`, `toDual_apply_eq_toDualMap_apply`, `hasFDerivWithinAt_iff_hasGradientWithinAt`, `HasFDerivAt.hasGradientAt`, `HasGradientWithinAt.hasFDerivWithinAt`
`toDualMap` 📖	CompOp	9 math math: `toLinearIsometry_toDual`, `toDualMap_apply_apply`, `toDualMap_apply`, `ProbabilityTheory.covarianceBilin_eq_covarianceBilinDual`, `nullSubmodule_le_ker_toDualMap_left`, `toContinuousLinearMap_toDualMap`, `toDual_apply_eq_toDualMap_apply`, `MeasureTheory.charFun_eq_charFunDual_toDualMap`, `nullSubmodule_le_ker_toDualMap_right`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousLinearMapOfBilin_apply` 📖	mathematical	—	`Inner.inner` `toInner` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `toNormedSpace` `ContinuousLinearMap.funLike` `continuousLinearMapOfBilin` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `RCLike.innerProductSpace` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `starRingEnd` `RCLike.toStarRing` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.addCommMonoid` `IsTopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `ContinuousLinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Ring.uniformContinuousConstSMul` `NormedRing.toRing` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `continuousLinearMapOfBilin.eq_1` `ContinuousLinearMap.coe_comp'` `ContinuousLinearEquiv.coe_coe` `LinearIsometryEquiv.coe_toContinuousLinearEquiv` `RingHomInvPair.instStarRingEnd` `RingHomIsometric.ids` `toDual_symm_apply`
`continuousLinearMapOfBilin_zero` 📖	mathematical	—	`continuousLinearMapOfBilin` `ContinuousLinearMap` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `starRingEnd` `RCLike.toStarRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedSpace.toModule` `toNormedSpace` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `RCLike.innerProductSpace` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.addCommMonoid` `IsTopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `ContinuousLinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Ring.uniformContinuousConstSMul` `NormedRing.toRing` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `ContinuousLinearMap.zero`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `ContinuousLinearMap.comp_zero`
`ext_inner_left_basis` 📖	—	`Inner.inner` `toInner` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `Module.Basis` `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` `toNormedSpace` `Module.Basis.instFunLike`	—	—	`RingHomIsometric.ids` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `LinearIsometry.map_eq_iff` `ContinuousLinearMap.coe_injective` `Module.Basis.ext` `inner_conj_symm`
`ext_inner_right_basis` 📖	—	`Inner.inner` `toInner` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `Module.Basis` `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` `toNormedSpace` `Module.Basis.instFunLike`	—	—	`ext_inner_left_basis` `inner_conj_symm`
`innerSL_norm` 📖	mathematical	—	`Norm.norm` `ContinuousLinearMap` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `starRingEnd` `RCLike.toStarRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedSpace.toModule` `toNormedSpace` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `RCLike.innerProductSpace` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.addCommMonoid` `IsTopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `ContinuousLinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Ring.uniformContinuousConstSMul` `NormedRing.toRing` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `ContinuousLinearMap.hasOpNorm` `ContinuousLinearMap.toSeminormedAddCommGroup` `DenselyNormedField.toNontriviallyNormedField` `RingHomIsometric.ids` `ContinuousLinearMap.toNormedSpace` `NontriviallyNormedField.toNormedField` `innerSL` `Real` `Real.instOne`	—	`RingHomIsometric.ids` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `LinearIsometry.norm_toContinuousLinearMap` `RingHomIsometric.starRingEnd` `CStarRing.to_normedStarGroup` `RCLike.instCStarRing`
`instIsContPerfPairRealInnerₗOfCompleteSpace` 📖	mathematical	—	`LinearMap.IsContPerfPair` `Real` `Real.commRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `toNormedSpace` `Real.instRCLike` `SeminormedAddCommGroup.toPseudoMetricSpace` `innerₗ`	—	`continuous_inner` `LinearIsometryEquiv.bijective` `RingHomInvPair.instStarRingEnd` `RingHomIsometric.ids` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SMulCommClass.symm` `Continuous.comp` `Continuous.prodMk_left` `LinearMap.ext` `flip_innerₗ` `ContinuousLinearMap.cont`
`nullSubmodule_le_ker_toDualMap_left` 📖	mathematical	—	`Submodule` `Ring.toSemiring` `SeminormedRing.toRing` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `toNormedSpace` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `nullSubmodule` `NormedSpace.toIsBoundedSMul` `LinearMap.ker` `StrongDual` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `ContinuousLinearMap.toSeminormedAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `DenselyNormedField.toNontriviallyNormedField` `RCLike.innerProductSpace` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomIsometric.ids` `ContinuousLinearMap.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Algebra.to_smulCommClass` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Ring.uniformContinuousConstSMul` `NormedRing.toRing` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `starRingEnd` `RCLike.toStarRing` `LinearIsometry.toLinearMap` `toDualMap`	—	`NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.ext` `RingHomIsometric.ids` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `inner_eq_zero_of_left`
`nullSubmodule_le_ker_toDualMap_right` 📖	mathematical	—	`Submodule` `Ring.toSemiring` `SeminormedRing.toRing` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `toNormedSpace` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `nullSubmodule` `NormedSpace.toIsBoundedSMul` `LinearMap.ker` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `ContinuousLinearMap.toLinearMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedRing.toPseudoMetricSpace` `DFunLike.coe` `LinearIsometry` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `starRingEnd` `RCLike.toStarRing` `StrongDual` `ContinuousLinearMap.toSeminormedAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `DenselyNormedField.toNontriviallyNormedField` `RCLike.innerProductSpace` `RingHomIsometric.ids` `ContinuousLinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Ring.uniformContinuousConstSMul` `NormedRing.toRing` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `LinearIsometry.instFunLike` `toDualMap`	—	`NormedSpace.toIsBoundedSMul` `inner_eq_zero_of_right` `mem_nullSubmodule_iff`
`rank_rankOne` 📖	mathematical	—	`LinearMap.rank` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `toNormedSpace` `ContinuousLinearMap.toLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `AddCommGroup.toAddCommMonoid` `DFunLike.coe` `ContinuousLinearMap` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `starRingEnd` `RCLike.toStarRing` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `ContinuousLinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.funLike` `ContinuousLinearMap.addCommGroup` `ContinuousLinearMap.topologicalAddGroup` `ContinuousLinearMap.toSeminormedAddCommGroup` `DenselyNormedField.toNontriviallyNormedField` `RingHomIsometric.ids` `ContinuousLinearMap.smulCommClass` `ContinuousLinearMap.continuousConstSMul` `rankOne` `Cardinal` `Cardinal.instOne`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.topologicalAddGroup` `RingHomIsometric.ids` `ContinuousLinearMap.smulCommClass` `ContinuousLinearMap.continuousConstSMul` `LinearMap.rank.eq_1` `IsScalarTower.left` `IsBoundedSMul.continuousSMul` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Algebra.to_smulCommClass` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `rankOne_def` `RingHomSurjective.ids` `ContinuousLinearMap.range_smulRight_apply` `Iff.not` `map_eq_zero_iff` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearIsometryClass.toSemilinearMapClass` `LinearIsometry.instSemilinearIsometryClass` `LinearIsometry.injective` `Module.rank_eq_one_iff_finrank_eq_one` `finrank_span_singleton`
`toContinuousLinearMap_toDualMap` 📖	mathematical	—	`LinearIsometry.toContinuousLinearMap` `StrongDual` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toPseudoMetricSpace` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `toNormedSpace` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `starRingEnd` `RCLike.toStarRing` `ContinuousLinearMap.toSeminormedAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `DenselyNormedField.toNontriviallyNormedField` `RCLike.innerProductSpace` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomIsometric.ids` `ContinuousLinearMap.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Algebra.to_smulCommClass` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Ring.uniformContinuousConstSMul` `NormedRing.toRing` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `toDualMap` `innerSL`	—	`RingHomIsometric.ids` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup`
`toDualMap_apply` 📖	mathematical	—	`DFunLike.coe` `StrongDual` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toPseudoMetricSpace` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `toNormedSpace` `ContinuousLinearMap.funLike` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearIsometry` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `starRingEnd` `RCLike.toStarRing` `ContinuousLinearMap.toSeminormedAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `DenselyNormedField.toNontriviallyNormedField` `RCLike.innerProductSpace` `RingHomIsometric.ids` `ContinuousLinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Ring.uniformContinuousConstSMul` `NormedRing.toRing` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `LinearIsometry.instFunLike` `toDualMap` `Inner.inner` `toInner`	—	`toDualMap_apply_apply`
`toDualMap_apply_apply` 📖	mathematical	—	`DFunLike.coe` `StrongDual` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toPseudoMetricSpace` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `toNormedSpace` `ContinuousLinearMap.funLike` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearIsometry` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `starRingEnd` `RCLike.toStarRing` `ContinuousLinearMap.toSeminormedAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `DenselyNormedField.toNontriviallyNormedField` `RCLike.innerProductSpace` `RingHomIsometric.ids` `ContinuousLinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Ring.uniformContinuousConstSMul` `NormedRing.toRing` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `LinearIsometry.instFunLike` `toDualMap` `Inner.inner` `toInner`	—	`RingHomIsometric.ids` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup`
`toDual_apply` 📖	mathematical	—	`DFunLike.coe` `StrongDual` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `toNormedSpace` `ContinuousLinearMap.funLike` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearIsometryEquiv` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `starRingEnd` `RCLike.toStarRing` `RingHomInvPair.instStarRingEnd` `ContinuousLinearMap.toSeminormedAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `DenselyNormedField.toNontriviallyNormedField` `RCLike.innerProductSpace` `RingHomIsometric.ids` `ContinuousLinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Ring.uniformContinuousConstSMul` `NormedRing.toRing` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `toDual` `Inner.inner` `toInner`	—	`toDual_apply_apply`
`toDual_apply_apply` 📖	mathematical	—	`DFunLike.coe` `StrongDual` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `toNormedSpace` `ContinuousLinearMap.funLike` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearIsometryEquiv` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `starRingEnd` `RCLike.toStarRing` `RingHomInvPair.instStarRingEnd` `ContinuousLinearMap.toSeminormedAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `DenselyNormedField.toNontriviallyNormedField` `RCLike.innerProductSpace` `RingHomIsometric.ids` `ContinuousLinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Ring.uniformContinuousConstSMul` `NormedRing.toRing` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `toDual` `Inner.inner` `toInner`	—	`RingHomInvPair.instStarRingEnd` `RingHomIsometric.ids` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup`
`toDual_apply_eq_toDualMap_apply` 📖	mathematical	—	`DFunLike.coe` `LinearIsometryEquiv` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `starRingEnd` `RCLike.toStarRing` `RingHomInvPair.instStarRingEnd` `StrongDual` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `toNormedSpace` `ContinuousLinearMap.toSeminormedAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `DenselyNormedField.toNontriviallyNormedField` `RCLike.innerProductSpace` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomIsometric.ids` `ContinuousLinearMap.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Algebra.to_smulCommClass` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Ring.uniformContinuousConstSMul` `NormedRing.toRing` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `toDual` `LinearIsometry` `AddCommGroup.toAddCommMonoid` `LinearIsometry.instFunLike` `toDualMap`	—	`RingHomInvPair.instStarRingEnd` `RingHomIsometric.ids` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup`
`toDual_symm_apply` 📖	mathematical	—	`Inner.inner` `toInner` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `LinearIsometryEquiv` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `starRingEnd` `RCLike.toStarRing` `RingHomInvPair.instStarRingEnd` `StrongDual` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `toNormedSpace` `ContinuousLinearMap.toSeminormedAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `DenselyNormedField.toNontriviallyNormedField` `RCLike.innerProductSpace` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomIsometric.ids` `ContinuousLinearMap.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Algebra.to_smulCommClass` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Ring.uniformContinuousConstSMul` `NormedRing.toRing` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `LinearIsometryEquiv.symm` `toDual` `ContinuousLinearMap.funLike`	—	`RingHomInvPair.instStarRingEnd` `RingHomIsometric.ids` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `toDual_apply_apply` `LinearIsometryEquiv.apply_symm_apply`
`toLinearIsometry_toDual` 📖	mathematical	—	`LinearIsometryEquiv.toLinearIsometry` `StrongDual` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `toNormedSpace` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `starRingEnd` `RCLike.toStarRing` `RingHomInvPair.instStarRingEnd` `ContinuousLinearMap.toSeminormedAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `DenselyNormedField.toNontriviallyNormedField` `RCLike.innerProductSpace` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomIsometric.ids` `ContinuousLinearMap.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Algebra.to_smulCommClass` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Ring.uniformContinuousConstSMul` `NormedRing.toRing` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `toDual` `toDualMap`	—	`RingHomIsometric.ids` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `RingHomInvPair.instStarRingEnd`
`unique_continuousLinearMapOfBilin` 📖	mathematical	`Inner.inner` `toInner` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedSpace.toModule` `toNormedSpace` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `RCLike.innerProductSpace` `ContinuousLinearMap.funLike` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `starRingEnd` `RCLike.toStarRing` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.addCommMonoid` `IsTopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `ContinuousLinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Ring.uniformContinuousConstSMul` `NormedRing.toRing` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`continuousLinearMapOfBilin`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `ext_inner_right` `continuousLinearMapOfBilin_apply`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`innerSL_inj` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `starRingEnd` `RCLike.toStarRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `RCLike.innerProductSpace` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.addCommMonoid` `IsTopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `ContinuousLinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Ring.uniformContinuousConstSMul` `NormedRing.toRing` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `ContinuousLinearMap.funLike` `innerSL`	—	`RingHomIsometric.ids` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `LinearIsometry.injective`

---

← Back to Index