Documentation Verification Report

Inversion

📁 Source: Mathlib/Analysis/Fourier/Inversion.lean

Statistics

Metric	Count
Definitions	0
Theorems `fourierInv_fourier_eq`, `fourier_fourierInv_eq`, `fourier_inversion`, `fourier_inversion_inv`, `fourierInv_fourier_eq`, `fourier_fourierInv_eq`, `fourier_inversion`, `fourier_inversion_inv`, `tendsto_integral_cexp_sq_smul`, `tendsto_integral_gaussian_smul`, `tendsto_integral_gaussian_smul'`	11
Total	11

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fourierInv_fourier_eq` 📖	mathematical	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `MeasureTheory.Integrable` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpaceOfInnerProductSpace` `MeasureTheory.MeasureSpace.volume` `FourierTransform.fourier` `Real.instFourierTransform`	`FourierTransformInv.fourierInv` `Real.instFourierTransformInv`	—	`MeasureTheory.Integrable.fourierInv_fourier_eq` `continuousAt`
`fourier_fourierInv_eq` 📖	mathematical	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `MeasureTheory.Integrable` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpaceOfInnerProductSpace` `MeasureTheory.MeasureSpace.volume` `FourierTransform.fourier` `Real.instFourierTransform`	`FourierTransformInv.fourierInv` `Real.instFourierTransformInv`	—	`MeasureTheory.Integrable.fourier_fourierInv_eq` `continuousAt`
`fourier_inversion` 📖	mathematical	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `MeasureTheory.Integrable` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpaceOfInnerProductSpace` `MeasureTheory.MeasureSpace.volume` `FourierTransform.fourier` `Real.instFourierTransform`	`FourierTransformInv.fourierInv` `Real.instFourierTransformInv`	—	`fourierInv_fourier_eq`
`fourier_inversion_inv` 📖	mathematical	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `MeasureTheory.Integrable` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpaceOfInnerProductSpace` `MeasureTheory.MeasureSpace.volume` `FourierTransform.fourier` `Real.instFourierTransform`	`FourierTransformInv.fourierInv` `Real.instFourierTransformInv`	—	`fourier_fourierInv_eq`

MeasureTheory.Integrable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fourierInv_fourier_eq` 📖	mathematical	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpaceOfInnerProductSpace` `MeasureTheory.MeasureSpace.volume` `FourierTransform.fourier` `Real.instFourierTransform` `ContinuousAt`	`FourierTransformInv.fourierInv` `Real.instFourierTransformInv`	—	`tendsto_nhds_unique` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Nat.instAtLeastTwoHAddOfNat` `Filter.atTop_neBot` `instIsDirectedOrder` `Real.instIsOrderedRing` `Real.instArchimedean` `Real.tendsto_integral_gaussian_smul` `Real.tendsto_integral_gaussian_smul'`
`fourier_fourierInv_eq` 📖	mathematical	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpaceOfInnerProductSpace` `MeasureTheory.MeasureSpace.volume` `FourierTransform.fourier` `Real.instFourierTransform` `ContinuousAt`	`FourierTransformInv.fourierInv` `Real.instFourierTransformInv`	—	`Real.fourierInv_comm` `fourierInv_fourier_eq`
`fourier_inversion` 📖	mathematical	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpaceOfInnerProductSpace` `MeasureTheory.MeasureSpace.volume` `FourierTransform.fourier` `Real.instFourierTransform` `ContinuousAt`	`FourierTransformInv.fourierInv` `Real.instFourierTransformInv`	—	`fourierInv_fourier_eq`
`fourier_inversion_inv` 📖	mathematical	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpaceOfInnerProductSpace` `MeasureTheory.MeasureSpace.volume` `FourierTransform.fourier` `Real.instFourierTransform` `ContinuousAt`	`FourierTransformInv.fourierInv` `Real.instFourierTransformInv`	—	`fourier_fourierInv_eq`

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tendsto_integral_cexp_sq_smul` 📖	mathematical	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpaceOfInnerProductSpace` `MeasureTheory.MeasureSpace.volume`	`Filter.Tendsto` `Real` `MeasureTheory.integral` `NormedSpace.complexToReal` `Complex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Complex.instNormedField` `Complex.exp` `Complex.instMul` `Complex.instNeg` `Complex.ofReal` `instInv` `Monoid.toNatPow` `Norm.norm` `NormedAddCommGroup.toNorm` `Filter.atTop` `instPreorder` `nhds`	—	`MeasureTheory.tendsto_integral_filter_of_dominated_convergence` `instIsCountablyGenerated_atTop` `instOrderTopologyReal` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `instSecondCountableTopologyReal` `Filter.univ_mem'` `MeasureTheory.AEStronglyMeasurable.smul` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Continuous.aestronglyMeasurable` `BorelSpace.opensMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `secondCountableTopologyEither_of_right` `secondCountable_of_proper` `Complex.instProperSpace` `Continuous.cexp` `Continuous.comp'` `Continuous.fun_mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `continuous_const` `continuous_id'` `Continuous.pow` `Complex.continuous_ofReal` `Continuous.norm` `Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `Filter.Ici_mem_atTop` `Complex.ofReal_inv` `neg_mul` `norm_smul` `NormedSpace.toNormSMulClass` `Complex.norm_real` `one_mul` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `instIsOrderedRing` `abs_exp` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `mul_nonneg` `IsOrderedRing.toPosMulMono` `inv_nonneg_of_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `instIsStrictOrderedRing` `Even.pow_nonneg` `IsStrictOrderedRing.toIsOrderedRing` `AddGroup.existsAddOfLE` `Nat.instAtLeastTwoHAddOfNat` `even_two_mul` `norm_nonneg` `MeasureTheory.Integrable.norm` `neg_zero` `MulZeroClass.zero_mul` `Complex.exp_zero` `one_smul` `Filter.Tendsto.smul_const` `Filter.Tendsto.cexp` `Filter.Tendsto.mul_const` `Filter.Tendsto.neg` `IsTopologicalRing.toContinuousNeg` `Filter.Tendsto.ofReal` `tendsto_inv_atTop_zero`
`tendsto_integral_gaussian_smul` 📖	mathematical	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpaceOfInnerProductSpace` `MeasureTheory.MeasureSpace.volume` `FourierTransform.fourier` `instFourierTransform`	`Filter.Tendsto` `Real` `MeasureTheory.integral` `NormedSpace.complexToReal` `Complex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Complex.instNormedField` `Complex.instMul` `Complex.instPow` `Complex.ofReal` `pi` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Complex.instNatCast` `Module.finrank` `semiring` `normedField` `InnerProductSpace.toNormedSpace` `instRCLike` `instOfNatAtLeastTwo` `Nat.instAtLeastTwoHAddOfNat` `Complex.exp` `Complex.instNeg` `Monoid.toNatPow` `Norm.norm` `NormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Filter.atTop` `instPreorder` `nhds` `FourierTransformInv.fourierInv` `instFourierTransformInv`	—	`Nat.instAtLeastTwoHAddOfNat` `Algebra.to_smulCommClass` `Continuous.neg` `IsTopologicalRing.toContinuousNeg` `instIsTopologicalRingReal` `continuous_inner` `neg_neg` `VectorFourier.fourierIntegral_convergent_iff` `continuous_fourierChar` `Submonoid.smul_def` `fourierChar_apply` `smul_smul` `Complex.exp_add` `real_inner_comm` `Complex.ofReal_mul` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `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.mul_pf_left` `fourierInv_eq` `tendsto_integral_cexp_sq_smul` `Filter.Tendsto.congr'` `Filter.mp_mem` `Filter.Ioi_mem_atTop` `instNoTopOrderOfNoMaxOrder` `instNoMaxOrderOfNontrivial` `instIsOrderedRing` `instNontrivial` `Filter.univ_mem'` `GaussianFourier.integrable_cexp_neg_mul_sq_norm_add` `Complex.ofReal_inv` `Complex.inv_re` `Complex.normSq_ofReal` `div_self_mul_self'` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `instIsStrictOrderedRing` `neg_mul` `SMulCommClass.symm` `flip_innerₗ` `VectorFourier.integral_fourierIntegral_smul_eq_flip` `MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite` `instIsAddHaarMeasureVolume` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `secondCountable_of_proper` `FiniteDimensional.proper_real` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `fourier_gaussian_innerProductSpace'` `div_inv_eq_mul` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero`
`tendsto_integral_gaussian_smul'` 📖	mathematical	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpaceOfInnerProductSpace` `MeasureTheory.MeasureSpace.volume` `ContinuousAt`	`Filter.Tendsto` `Real` `MeasureTheory.integral` `NormedSpace.complexToReal` `Complex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Complex.instNormedField` `Complex.instMul` `Complex.instPow` `Complex.ofReal` `pi` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Complex.instNatCast` `Module.finrank` `semiring` `normedField` `InnerProductSpace.toNormedSpace` `instRCLike` `instOfNatAtLeastTwo` `Nat.instAtLeastTwoHAddOfNat` `Complex.exp` `Complex.instNeg` `Monoid.toNatPow` `Norm.norm` `NormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Filter.atTop` `instPreorder` `nhds`	—	`Nat.instAtLeastTwoHAddOfNat` `tendsto_integral_comp_smul_smul_of_integrable'` `instIsAddHaarMeasureVolume` `le_of_lt` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `instIsStrictOrderedRing` `rpow_pos_of_pos` `pi_pos` `exp_pos` `MeasureTheory.integral_const_mul` `GaussianFourier.integral_rexp_neg_mul_sq_norm` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass` `pow_one` `rpow_natCast` `rpow_sub` `rpow_mul` `pi_nonneg` `rpow_add` `Mathlib.Tactic.Ring.atom_pf'` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Meta.NormNum.IsNNRat.to_raw_eq` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Meta.NormNum.isNat_natCast` `Mathlib.Tactic.Ring.sub_pf` `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.add_pf_add_overlap` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Meta.NormNum.IsRat.to_raw_eq` `Mathlib.Meta.NormNum.isRat_mul` `Mathlib.Meta.NormNum.IsInt.to_isRat` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.IsNNRat.of_raw` `Mathlib.Meta.NormNum.IsNNRat.den_nz` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.IsRat.to_isInt` `Mathlib.Meta.NormNum.isRat_add` `Mathlib.Meta.NormNum.IsRat.of_raw` `Mathlib.Meta.NormNum.IsRat.den_nz` `Mathlib.Tactic.RingNF.nat_rawCast_1` `mul_one` `add_zero` `rpow_zero` `Filter.tendsto_const_mul_atTop_of_pos` `Filter.Tendsto.comp` `Filter.tendsto_pow_atTop` `instIsOrderedRing` `two_ne_zero` `tendsto_norm_cobounded_atTop` `Filter.Tendsto.const_mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero` `zero_lt_one` `instZeroLEOneClass` `NeZero.charZero_one` `neg_mul` `one_mul` `mul_rpow` `rpow_nonneg` `norm_nonneg` `mul_assoc` `mul_comm` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.IsRat.to_isNNRat` `MulZeroClass.mul_zero` `tendsto_rpow_atTop` `one_div` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `instNontrivial` `Filter.Tendsto.congr'` `Filter.mp_mem` `Filter.Ioi_mem_atTop` `instNoTopOrderOfNoMaxOrder` `instNoMaxOrderOfNontrivial` `Filter.univ_mem'` `Complex.coe_smul` `Complex.ofReal_mul` `Complex.ofReal_exp` `Complex.mul_cpow_ofReal_nonneg` `LT.lt.le` `Complex.ofReal_cpow` `div_eq_inv_mul` `Complex.ofReal_inv` `Nat.cast_one` `norm_smul` `NormedSpace.toNormSMulClass` `mul_pow` `sq_abs` `rpow_ofNat` `inv_mul_cancel₀` `rpow_one`

---

← Back to Index