Documentation Verification Report

QuaternionExponential

📁 Source: Mathlib/Analysis/Normed/Algebra/QuaternionExponential.lean

Statistics

Metric	Count
Definitions	0
Theorems `expSeries_even_of_imaginary`, `expSeries_odd_of_imaginary`, `exp_coe`, `exp_eq`, `exp_of_re_eq_zero`, `hasSum_expSeries_of_imaginary`, `im_exp`, `normSq_exp`, `norm_exp`, `re_exp`	10
Total	10

Quaternion

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`expSeries_even_of_imaginary` 📖	mathematical	`QuaternionAlgebra.re` `Real` `Real.instNeg` `Real.instOne` `Real.instZero`	`DFunLike.coe` `ContinuousMultilinearMap` `Quaternion` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.instField` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRing` `Real.commRing` `Algebra.toModule` `Semifield.toCommSemiring` `Ring.toSemiring` `algebra` `Algebra.id` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `instNormedDivisionRingReal` `ContinuousMultilinearMap.funLike` `NormedSpace.expSeries` `IsTopologicalDivisionRing.toIsTopologicalRing` `instDivisionRing` `Real.linearOrder` `Real.instIsStrictOrderedRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `coe` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `Norm.norm` `NormedDivisionRing.toNorm` `Real.instNatCast` `Nat.factorial`	—	`IsTopologicalDivisionRing.toIsTopologicalRing` `Real.instIsStrictOrderedRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `NormedSpace.expSeries_apply_eq` `sq_eq_neg_normSq` `pow_mul` `neg_pow` `normSq_eq_norm_mul_self` `sq` `coe_mul` `coe_pow` `coe_neg` `coe_mul_eq_smul` `div_eq_mul_inv` `Nat.cast_one` `Nat.instAtLeastTwoHAddOfNat` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.inv_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Tactic.Ring.inv_mul` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.RingNF.nat_rawCast_1` `pow_one` `mul_one` `Mathlib.Tactic.RingNF.mul_assoc_rev` `add_zero`
`expSeries_odd_of_imaginary` 📖	mathematical	`QuaternionAlgebra.re` `Real` `Real.instNeg` `Real.instOne` `Real.instZero`	`DFunLike.coe` `ContinuousMultilinearMap` `Quaternion` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.instField` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRing` `Real.commRing` `Algebra.toModule` `Semifield.toCommSemiring` `Ring.toSemiring` `algebra` `Algebra.id` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `instNormedDivisionRingReal` `ContinuousMultilinearMap.funLike` `NormedSpace.expSeries` `IsTopologicalDivisionRing.toIsTopologicalRing` `instDivisionRing` `Real.linearOrder` `Real.instIsStrictOrderedRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `instSMul` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `Norm.norm` `NormedDivisionRing.toNorm` `Real.instNatCast` `Nat.factorial`	—	`IsTopologicalDivisionRing.toIsTopologicalRing` `Real.instIsStrictOrderedRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `NormedSpace.expSeries_apply_eq` `eq_or_ne` `zero_pow` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `StarOrderedRing.toExistsAddOfLE` `Nat.instStarOrderedRing` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `smul_zero` `norm_zero` `MulZeroClass.mul_zero` `zero_div` `div_zero` `sq_eq_neg_normSq` `norm_ne_zero_iff` `pow_succ` `pow_mul` `neg_pow` `normSq_eq_norm_mul_self` `sq` `coe_mul_eq_smul` `Nat.cast_one` `Int.cast_pow` `Int.cast_neg` `Int.cast_one` `coe_pow` `coe_neg` `smul_smul` `mul_div_assoc` `div_div_cancel_left'` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.inv_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Tactic.Ring.inv_mul` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.pow_prod_atom` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_pow`
`exp_coe` 📖	mathematical	—	`NormedSpace.exp` `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` `instRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `instNormedDivisionRingReal` `IsTopologicalDivisionRing.toIsTopologicalRing` `instDivisionRing` `Real.instField` `Real.linearOrder` `Real.instIsStrictOrderedRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `coe` `Real.instRing` `Real.pseudoMetricSpace` `instIsTopologicalRingReal`	—	`Real.instIsStrictOrderedRing` `NonUnitalSeminormedRing.toIsTopologicalRing` `NormedSpace.map_exp` `RCLike.charZero_rclike` `Real.instCompleteSpace` `RingHom.instRingHomClass` `continuous_algebraMap` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul`
`exp_eq` 📖	mathematical	—	`NormedSpace.exp` `Quaternion` `Real` `Real.instZero` `Real.instOne` `Real.instNeg` `instRing` `Real.commRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `instNormedDivisionRingReal` `IsTopologicalDivisionRing.toIsTopologicalRing` `instDivisionRing` `Real.instField` `Real.linearOrder` `Real.instIsStrictOrderedRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `instSMul` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Real.instRing` `Real.pseudoMetricSpace` `instIsTopologicalRingReal` `QuaternionAlgebra.re` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `coe` `Real.cos` `Norm.norm` `NormedDivisionRing.toNorm` `im` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.sin`	—	`RCLike.charZero_rclike` `IsTopologicalDivisionRing.toIsTopologicalRing` `Real.instIsStrictOrderedRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `instIsTopologicalRingReal` `exp_of_re_eq_zero` `re_im` `coe_mul_eq_smul` `exp_coe` `NonUnitalSeminormedRing.toIsTopologicalRing` `NormedSpace.exp_add_of_commute` `instCompleteSpaceReal` `Algebra.commutes` `re_add_im`
`exp_of_re_eq_zero` 📖	mathematical	`QuaternionAlgebra.re` `Real` `Real.instNeg` `Real.instOne` `Real.instZero`	`NormedSpace.exp` `Quaternion` `instRing` `Real.commRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `instNormedDivisionRingReal` `IsTopologicalDivisionRing.toIsTopologicalRing` `instDivisionRing` `Real.instField` `Real.linearOrder` `Real.instIsStrictOrderedRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `coe` `Real.cos` `Norm.norm` `NormedDivisionRing.toNorm` `instSMul` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.sin`	—	`IsTopologicalDivisionRing.toIsTopologicalRing` `Real.instIsStrictOrderedRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `NormedSpace.exp_eq_tsum` `RCLike.charZero_rclike` `HasSum.tsum_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional` `hasSum_expSeries_of_imaginary` `Real.hasSum_cos` `Real.hasSum_sin`
`hasSum_expSeries_of_imaginary` 📖	mathematical	`QuaternionAlgebra.re` `Real` `Real.instNeg` `Real.instOne` `Real.instZero` `HasSum` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `Norm.norm` `Quaternion` `NormedDivisionRing.toNorm` `instNormedDivisionRingReal` `Real.instNatCast` `Nat.factorial` `SummationFilter.unconditional`	`ESeminormedAddCommMonoid.toAddCommMonoid` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instNormedAddCommGroupReal` `DFunLike.coe` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.instField` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRing` `Real.commRing` `Algebra.toModule` `Semifield.toCommSemiring` `Ring.toSemiring` `algebra` `Algebra.id` `ContinuousMultilinearMap.funLike` `NormedSpace.expSeries` `IsTopologicalDivisionRing.toIsTopologicalRing` `instDivisionRing` `Real.linearOrder` `Real.instIsStrictOrderedRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `coe` `instSMul` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring`	—	`hasSum_coe` `HasSum.smul_const` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `HasSum.div_const` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `HasSum.even_add_odd` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalDivisionRing.toIsTopologicalRing` `Real.instIsStrictOrderedRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `expSeries_even_of_imaginary` `expSeries_odd_of_imaginary`
`im_exp` 📖	mathematical	—	`im` `Real` `Real.commRing` `NormedSpace.exp` `Quaternion` `Real.instZero` `Real.instOne` `Real.instNeg` `instRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `instNormedDivisionRingReal` `IsTopologicalDivisionRing.toIsTopologicalRing` `instDivisionRing` `Real.instField` `Real.linearOrder` `Real.instIsStrictOrderedRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `instSMul` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Real.instMul` `Real.instRing` `Real.pseudoMetricSpace` `instIsTopologicalRingReal` `QuaternionAlgebra.re` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.sin` `Norm.norm` `NormedDivisionRing.toNorm`	—	`IsTopologicalDivisionRing.toIsTopologicalRing` `Real.instIsStrictOrderedRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `instIsTopologicalRingReal` `exp_eq` `smul_add` `smul_smul` `im_add` `im_smul` `smul_zero` `zero_add`
`normSq_exp` 📖	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` `NormedSpace.exp` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `instNormedDivisionRingReal` `IsTopologicalDivisionRing.toIsTopologicalRing` `instDivisionRing` `Real.instField` `Real.linearOrder` `Real.instIsStrictOrderedRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Monoid.toNatPow` `Real.instMonoid` `Real.instRing` `Real.pseudoMetricSpace` `instIsTopologicalRingReal` `QuaternionAlgebra.re` `Real.instNeg` `Real.instOne` `Real.instZero`	—	`IsTopologicalDivisionRing.toIsTopologicalRing` `Real.instIsStrictOrderedRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `instIsTopologicalRingReal` `exp_eq` `normSq_smul` `eq_or_ne` `Real.cos_zero` `Real.sin_zero` `div_zero` `zero_smul` `add_zero` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass` `one_pow` `zero_pow` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `normSq_add` `star_smul` `coe_mul_eq_smul` `re_smul` `re_star` `re_im` `smul_zero` `MulZeroClass.mul_zero` `div_pow` `normSq_coe` `normSq_eq_norm_mul_self` `sq` `div_mul_cancel₀` `pow_ne_zero` `isReduced_of_noZeroDivisors` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `Real.cos_sq_add_sin_sq` `mul_one`
`norm_exp` 📖	mathematical	—	`Norm.norm` `Quaternion` `Real` `Real.instZero` `Real.instOne` `Real.instNeg` `NormedDivisionRing.toNorm` `instNormedDivisionRingReal` `NormedSpace.exp` `instRing` `Real.commRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `instDivisionRing` `Real.instField` `Real.linearOrder` `Real.instIsStrictOrderedRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Real.norm` `Real.instRing` `Real.pseudoMetricSpace` `instIsTopologicalRingReal` `QuaternionAlgebra.re`	—	`IsTopologicalDivisionRing.toIsTopologicalRing` `Real.instIsStrictOrderedRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `instIsTopologicalRingReal` `norm_eq_sqrt_real_inner` `inner_self` `normSq_exp` `Real.sqrt_sq_eq_abs` `Real.norm_eq_abs`
`re_exp` 📖	mathematical	—	`QuaternionAlgebra.re` `Real` `Real.instNeg` `Real.instOne` `Real.instZero` `NormedSpace.exp` `Quaternion` `instRing` `Real.commRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `instNormedDivisionRingReal` `IsTopologicalDivisionRing.toIsTopologicalRing` `instDivisionRing` `Real.instField` `Real.linearOrder` `Real.instIsStrictOrderedRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Real.instMul` `Real.instRing` `Real.pseudoMetricSpace` `instIsTopologicalRingReal` `Real.cos` `Norm.norm` `NormedDivisionRing.toNorm` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `instNormedAddCommGroupReal` `coe`	—	`IsTopologicalDivisionRing.toIsTopologicalRing` `Real.instIsStrictOrderedRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `instIsTopologicalRingReal` `exp_eq` `smul_add` `MulZeroClass.mul_zero` `add_zero` `sub_re_self`

---

← Back to Index