Quaternion

📁 Source: Mathlib/Analysis/Quaternion.lean

Statistics

Metric	Count
Definitions `coeComplex`, `instCoeComplexReal`, `instInnerProductSpaceReal`, `instInnerReal`, `instNormedAddCommGroupReal`, `instNormedAlgebraReal`, `instNormedDivisionRingReal`, `linearIsometryEquivTuple`, `ofComplex`, `termℍ`	10
Theorems `coeComplex_add`, `coeComplex_coe`, `coeComplex_imI`, `coeComplex_imJ`, `coeComplex_imK`, `coeComplex_mul`, `coeComplex_one`, `coeComplex_re`, `coeComplex_zero`, `coe_ofComplex`, `coe_real_complex_mul`, `continuous_coe`, `continuous_im`, `continuous_imI`, `continuous_imJ`, `continuous_imK`, `continuous_normSq`, `continuous_re`, `hasSum_coe`, `imI_coeComplex`, `imJ_coeComplex`, `imK_coeComplex`, `inner_def`, `inner_self`, `instCStarRingReal`, `instCompleteSpaceReal`, `instNormOneClassReal`, `linearIsometryEquivTuple_apply`, `linearIsometryEquivTuple_symm_apply`, `nnnorm_coe`, `nnnorm_star`, `normSq_eq_norm_mul_self`, `norm_coe`, `norm_star`, `norm_toLp_equivTuple`, `re_coeComplex`, `summable_coe`, `tsum_coe`	38
Total	48

Quaternion

Definitions

Name	Category	Theorems
`coeComplex` 📖	CompOp	15 math math: `coeComplex_re`, `coeComplex_mul`, `imI_coeComplex`, `coeComplex_add`, `coeComplex_zero`, `coeComplex_imK`, `re_coeComplex`, `coeComplex_coe`, `imK_coeComplex`, `coeComplex_imJ`, `imJ_coeComplex`, `coeComplex_imI`, `coe_ofComplex`, `coeComplex_one`, `coe_real_complex_mul`
`instCoeComplexReal` 📖	CompOp	—
`instInnerProductSpaceReal` 📖	CompOp	—
`instInnerReal` 📖	CompOp	2 math math: `inner_def`, `inner_self`
`instNormedAddCommGroupReal` 📖	CompOp	11 math math: `nnnorm_star`, `norm_coe`, `re_exp`, `normSq_eq_norm_mul_self`, `summable_coe`, `tsum_coe`, `hasSum_expSeries_of_imaginary`, `instNormOneClassReal`, `hasSum_coe`, `nnnorm_coe`, `norm_star`
`instNormedAlgebraReal` 📖	CompOp	—
`instNormedDivisionRingReal` 📖	CompOp	24 math math: `continuous_imI`, `instCStarRingReal`, `linearIsometryEquivTuple_symm_apply`, `expSeries_odd_of_imaginary`, `continuous_imJ`, `instCompleteSpaceReal`, `exp_of_re_eq_zero`, `re_exp`, `expSeries_even_of_imaginary`, `normSq_exp`, `im_exp`, `summable_coe`, `tsum_coe`, `continuous_im`, `norm_exp`, `continuous_coe`, `linearIsometryEquivTuple_apply`, `hasSum_coe`, `continuous_imK`, `continuous_normSq`, `continuous_re`, `exp_coe`, `norm_toLp_equivTuple`, `exp_eq`
`linearIsometryEquivTuple` 📖	CompOp	2 math math: `linearIsometryEquivTuple_symm_apply`, `linearIsometryEquivTuple_apply`
`ofComplex` 📖	CompOp	1 math math: `coe_ofComplex`
`termℍ` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeComplex_add` 📖	mathematical	—	`coeComplex` `Complex` `Complex.instAdd` `Quaternion` `Real` `Real.instZero` `Real.instOne` `Real.instNeg` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRing` `Real.commRing`	—	`ext` `add_zero`
`coeComplex_coe` 📖	mathematical	—	`coeComplex` `Complex.ofReal` `coe` `Real` `Real.commRing`	—	—
`coeComplex_imI` 📖	mathematical	—	`QuaternionAlgebra.imI` `Real` `Real.instNeg` `Real.instOne` `Real.instZero` `coeComplex` `Complex.im`	—	`imI_coeComplex`
`coeComplex_imJ` 📖	mathematical	—	`QuaternionAlgebra.imJ` `Real` `Real.instNeg` `Real.instOne` `Real.instZero` `coeComplex`	—	`imJ_coeComplex`
`coeComplex_imK` 📖	mathematical	—	`QuaternionAlgebra.imK` `Real` `Real.instNeg` `Real.instOne` `Real.instZero` `coeComplex`	—	`imK_coeComplex`
`coeComplex_mul` 📖	mathematical	—	`coeComplex` `Complex` `Complex.instMul` `Quaternion` `Real` `Real.instZero` `Real.instOne` `Real.instNeg` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRing` `Real.commRing`	—	`ext` `re_mul` `MulZeroClass.mul_zero` `sub_zero` `imI_mul` `add_zero` `imJ_mul` `sub_self` `MulZeroClass.zero_mul` `imK_mul`
`coeComplex_one` 📖	mathematical	—	`coeComplex` `Complex` `Complex.instOne` `Quaternion` `Real` `Real.instZero` `Real.instOne` `Real.instNeg` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `instRing` `Real.commRing`	—	—
`coeComplex_re` 📖	mathematical	—	`QuaternionAlgebra.re` `Real` `Real.instNeg` `Real.instOne` `Real.instZero` `coeComplex` `Complex.re`	—	`re_coeComplex`
`coeComplex_zero` 📖	mathematical	—	`coeComplex` `Complex` `Complex.instZero` `Quaternion` `Real` `Real.instZero` `Real.instOne` `Real.instNeg` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRing` `Real.commRing`	—	—
`coe_ofComplex` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Real` `Complex` `Quaternion` `Real.instZero` `Real.instOne` `Real.instNeg` `Real.instCommSemiring` `Complex.instSemiring` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `instDivisionRing` `Real.instField` `Real.linearOrder` `Real.instIsStrictOrderedRing` `NormedAlgebra.toAlgebra` `Real.normedField` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `RCLike.toNormedAlgebra` `Complex.instRCLike` `algebra` `Real.commRing` `Algebra.id` `AlgHom.funLike` `ofComplex` `coeComplex`	—	`Real.instIsStrictOrderedRing`
`coe_real_complex_mul` 📖	mathematical	—	`Real` `Quaternion` `Real.instZero` `Real.instOne` `Real.instNeg` `instSMul` `Real.commRing` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `coeComplex` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRing` `coe`	—	`ext` `re_mul` `MulZeroClass.zero_mul` `sub_zero` `MulZeroClass.mul_zero` `imI_mul` `add_zero` `imJ_mul` `sub_self` `imK_mul`
`continuous_coe` 📖	mathematical	—	`Continuous` `Real` `Quaternion` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Real.commRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `instNormedDivisionRingReal` `coe`	—	`continuous_algebraMap` `Real.instIsStrictOrderedRing` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul`
`continuous_im` 📖	mathematical	—	`Continuous` `Quaternion` `Real` `Real.instZero` `Real.instOne` `Real.instNeg` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Real.commRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `instNormedDivisionRingReal` `im`	—	`Continuous.sub` `IsTopologicalAddGroup.to_continuousSub` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `continuous_id` `Continuous.comp` `continuous_coe` `continuous_re`
`continuous_imI` 📖	mathematical	—	`Continuous` `Quaternion` `Real` `Real.instZero` `Real.instOne` `Real.instNeg` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `instNormedDivisionRingReal` `Real.pseudoMetricSpace` `QuaternionAlgebra.imI`	—	`Continuous.comp` `Nat.instAtLeastTwoHAddOfNat` `RingHomInvPair.ids` `fact_one_le_two_ennreal` `PiLp.continuous_apply` `LinearIsometryEquiv.continuous`
`continuous_imJ` 📖	mathematical	—	`Continuous` `Quaternion` `Real` `Real.instZero` `Real.instOne` `Real.instNeg` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `instNormedDivisionRingReal` `Real.pseudoMetricSpace` `QuaternionAlgebra.imJ`	—	`Continuous.comp` `Nat.instAtLeastTwoHAddOfNat` `RingHomInvPair.ids` `fact_one_le_two_ennreal` `PiLp.continuous_apply` `LinearIsometryEquiv.continuous`
`continuous_imK` 📖	mathematical	—	`Continuous` `Quaternion` `Real` `Real.instZero` `Real.instOne` `Real.instNeg` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `instNormedDivisionRingReal` `Real.pseudoMetricSpace` `QuaternionAlgebra.imK`	—	`Continuous.comp` `Nat.instAtLeastTwoHAddOfNat` `RingHomInvPair.ids` `fact_one_le_two_ennreal` `PiLp.continuous_apply` `LinearIsometryEquiv.continuous`
`continuous_normSq` 📖	mathematical	—	`Continuous` `Quaternion` `Real` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Real.commRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `instNormedDivisionRingReal` `Real.pseudoMetricSpace` `DFunLike.coe` `MonoidWithZeroHom` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `instRing` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidWithZeroHom.funLike` `normSq`	—	`Continuous.fun_mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `continuous_norm`
`continuous_re` 📖	mathematical	—	`Continuous` `Quaternion` `Real` `Real.instZero` `Real.instOne` `Real.instNeg` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `instNormedDivisionRingReal` `Real.pseudoMetricSpace` `QuaternionAlgebra.re`	—	`Continuous.comp` `Nat.instAtLeastTwoHAddOfNat` `RingHomInvPair.ids` `fact_one_le_two_ennreal` `PiLp.continuous_apply` `LinearIsometryEquiv.continuous`
`hasSum_coe` 📖	mathematical	—	`HasSum` `Quaternion` `Real` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Real.commRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `instNormedDivisionRingReal` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instNormedAddCommGroupReal` `coe` `Real.instAddCommMonoid` `Real.pseudoMetricSpace`	—	`HasSum.map` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `continuous_re` `Real.instIsStrictOrderedRing` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `continuous_algebraMap` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul`
`imI_coeComplex` 📖	mathematical	—	`QuaternionAlgebra.imI` `Real` `Real.instNeg` `Real.instOne` `Real.instZero` `coeComplex` `Complex.im`	—	—
`imJ_coeComplex` 📖	mathematical	—	`QuaternionAlgebra.imJ` `Real` `Real.instNeg` `Real.instOne` `Real.instZero` `coeComplex`	—	—
`imK_coeComplex` 📖	mathematical	—	`QuaternionAlgebra.imK` `Real` `Real.instNeg` `Real.instOne` `Real.instZero` `coeComplex`	—	—
`inner_def` 📖	mathematical	—	`Inner.inner` `Real` `Quaternion` `Real.instZero` `Real.instOne` `Real.instNeg` `instInnerReal` `QuaternionAlgebra.re` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRing` `Real.commRing` `Star.star` `instStar`	—	—
`inner_self` 📖	mathematical	—	`Inner.inner` `Real` `Quaternion` `Real.instZero` `Real.instOne` `Real.instNeg` `instInnerReal` `DFunLike.coe` `MonoidWithZeroHom` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Real.commRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `instRing` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidWithZeroHom.funLike` `normSq`	—	—
`instCStarRingReal` 📖	mathematical	—	`CStarRing` `Quaternion` `Real` `Real.instZero` `Real.instOne` `Real.instNeg` `NormedRing.toNonUnitalNormedRing` `NormedDivisionRing.toNormedRing` `instNormedDivisionRingReal` `instStarRing` `Real.commRing`	—	`le_of_eq` `norm_mul` `NormedDivisionRing.toNormMulClass` `norm_star`
`instCompleteSpaceReal` 📖	mathematical	—	`CompleteSpace` `Quaternion` `Real` `Real.instZero` `Real.instOne` `Real.instNeg` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `instNormedDivisionRingReal`	—	`completeSpace_congr` `fact_one_le_two_ennreal` `RingHomInvPair.ids` `ContinuousLinearEquiv.isUniformEmbedding` `SeminormedAddCommGroup.to_isUniformAddGroup` `PiLp.completeSpace` `Real.instCompleteSpace`
`instNormOneClassReal` 📖	mathematical	—	`NormOneClass` `Quaternion` `Real` `Real.instZero` `Real.instOne` `Real.instNeg` `NormedAddCommGroup.toNorm` `instNormedAddCommGroupReal` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `instRing` `Real.commRing`	—	`norm_eq_sqrt_real_inner` `inner_self` `MonoidWithZeroHom.map_one` `Real.sqrt_one`
`linearIsometryEquivTuple_apply` 📖	mathematical	—	`DFunLike.coe` `LinearIsometryEquiv` `Real` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Quaternion` `Real.instZero` `Real.instOne` `Real.instNeg` `EuclideanSpace` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `NormedDivisionRing.toNormedRing` `instNormedDivisionRingReal` `PiLp.seminormedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `Fin.fintype` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `instModule` `Real.commRing` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `WithLp.instModule` `Pi.addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `SeminormedCommRing.toSeminormedRing` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `linearIsometryEquivTuple` `WithLp.toLp` `Matrix.vecCons` `QuaternionAlgebra.re` `QuaternionAlgebra.imI` `QuaternionAlgebra.imJ` `QuaternionAlgebra.imK` `Matrix.vecEmpty`	—	`RingHomInvPair.ids` `fact_one_le_two_ennreal`
`linearIsometryEquivTuple_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearIsometryEquiv` `Real` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EuclideanSpace` `Quaternion` `Real.instZero` `Real.instOne` `Real.instNeg` `PiLp.seminormedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `Fin.fintype` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `NormedDivisionRing.toNormedRing` `instNormedDivisionRingReal` `WithLp.instModule` `Pi.addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `SeminormedCommRing.toSeminormedRing` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `instModule` `Real.commRing` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `LinearIsometryEquiv.symm` `linearIsometryEquivTuple` `WithLp.ofLp`	—	`RingHomInvPair.ids` `fact_one_le_two_ennreal`
`nnnorm_coe` 📖	mathematical	—	`NNNorm.nnnorm` `Quaternion` `Real` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Real.commRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `instNormedAddCommGroupReal` `coe` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing`	—	`norm_coe`
`nnnorm_star` 📖	mathematical	—	`NNNorm.nnnorm` `Quaternion` `Real` `Real.instZero` `Real.instOne` `Real.instNeg` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `instNormedAddCommGroupReal` `Star.star` `instStar` `Real.commRing`	—	`norm_star`
`normSq_eq_norm_mul_self` 📖	mathematical	—	`DFunLike.coe` `MonoidWithZeroHom` `Quaternion` `Real` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Real.commRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `instRing` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidWithZeroHom.funLike` `normSq` `Real.instMul` `Norm.norm` `Real.instZero` `Real.instOne` `Real.instNeg` `NormedAddCommGroup.toNorm` `instNormedAddCommGroupReal`	—	`inner_self` `real_inner_self_eq_norm_mul_norm`
`norm_coe` 📖	mathematical	—	`Norm.norm` `Quaternion` `Real` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Real.commRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `NormedAddCommGroup.toNorm` `instNormedAddCommGroupReal` `coe` `Real.norm`	—	`norm_eq_sqrt_real_inner` `inner_self` `normSq_coe` `Real.sqrt_sq_eq_abs` `Real.norm_eq_abs`
`norm_star` 📖	mathematical	—	`Norm.norm` `Quaternion` `Real` `Real.instZero` `Real.instOne` `Real.instNeg` `NormedAddCommGroup.toNorm` `instNormedAddCommGroupReal` `Star.star` `instStar` `Real.commRing`	—	`norm_eq_sqrt_real_inner` `normSq_star`
`norm_toLp_equivTuple` 📖	mathematical	—	`Norm.norm` `WithLp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `PiLp.instNorm` `Real` `Fin.fintype` `Real.norm` `WithLp.toLp` `DFunLike.coe` `Equiv` `Quaternion` `Real.instZero` `Real.instOne` `Real.instNeg` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivTuple` `NormedDivisionRing.toNorm` `instNormedDivisionRingReal`	—	`Nat.instAtLeastTwoHAddOfNat` `fact_one_le_two_ennreal` `norm_eq_sqrt_real_inner` `inner_self` `normSq_def'` `PiLp.inner_apply` `Fin.sum_univ_four` `TrivialStar.star_trivial` `instTrivialStarReal`
`re_coeComplex` 📖	mathematical	—	`QuaternionAlgebra.re` `Real` `Real.instNeg` `Real.instOne` `Real.instZero` `coeComplex` `Complex.re`	—	—
`summable_coe` 📖	mathematical	—	`Summable` `Quaternion` `Real` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Real.commRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `instNormedDivisionRingReal` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instNormedAddCommGroupReal` `coe` `Real.instAddCommMonoid` `Real.pseudoMetricSpace`	—	`Summable.map_iff_of_leftInverse` `Real.instIsStrictOrderedRing` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `continuous_algebraMap` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `continuous_re` `re_coe`
`tsum_coe` 📖	mathematical	—	`tsum` `Quaternion` `Real` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Real.commRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `instNormedDivisionRingReal` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instNormedAddCommGroupReal` `coe` `Real.instAddCommMonoid` `Real.pseudoMetricSpace`	—	`Function.LeftInverse.map_tsum` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `continuous_algebraMap` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `continuous_re` `re_coe`

---

← Back to Index