Documentation Verification Report

Laplacian

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

Statistics

Metric	Count
Definitions `laplacian`, `instLaplacian`, `laplacianWithin`, `«termΔ[_]_»`, `Laplacian`, `bilinearIteratedFDerivTwo`, `bilinearIteratedFDerivWithinTwo`, `tensorIteratedFDerivTwo`, `tensorIteratedFDerivWithinTwo`	9
Theorems `laplacianWithin_add_nhdsWithin`, `laplacian_CLM_comp_left`, `laplacian_CLM_comp_left_nhds`, `laplacian_add`, `laplacian_add_nhds`, `laplacianWithin_CLM_comp_left`, `laplacianWithin_CLM_comp_left_nhds`, `laplacianWithin_add`, `laplacianWithin_CLE_comp_left`, `laplacianWithin_congr_nhdsWithin`, `laplacianWithin_eq_iteratedDerivWithin_real`, `laplacianWithin_eq_iteratedFDerivWithin_complexPlane`, `laplacianWithin_eq_iteratedFDerivWithin_orthonormalBasis`, `laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis`, `laplacianWithin_smul`, `laplacianWithin_smul_nhds`, `laplacianWithin_univ`, `laplacian_CLE_comp_left`, `laplacian_congr_nhds`, `laplacian_eq_iteratedDeriv_real`, `laplacian_eq_iteratedFDeriv_complexPlane`, `laplacian_eq_iteratedFDeriv_orthonormalBasis`, `laplacian_eq_iteratedFDeriv_stdOrthonormalBasis`, `laplacian_smul`, `laplacian_smul_nhds`, `bilinearIteratedFDerivTwo_eq_iteratedFDeriv`, `bilinearIteratedFDerivWithinTwo_eq_iteratedFDeriv`, `tensorIteratedFDerivTwo_eq_iteratedFDeriv`, `tensorIteratedFDerivWithinTwo_eq_iteratedFDerivWithin`	29
Total	38

ContDiffAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`laplacianWithin_add_nhdsWithin` 📖	mathematical	`ContDiffWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `WithTop` `ENat` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Nat.instAtLeastTwoHAddOfNat` `UniqueDiffOn` `Real.semiring` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set` `Set.instMembership`	`Filter.EventuallyEq` `nhdsWithin` `InnerProductSpace.laplacianWithin` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`Nat.instAtLeastTwoHAddOfNat` `Set.insert_eq_of_mem` `Filter.mp_mem` `eventually_mem_nhdsWithin` `ContDiffWithinAt.eventually` `Filter.univ_mem'` `ContDiffWithinAt.laplacianWithin_add`
`laplacian_CLM_comp_left` 📖	mathematical	`ContDiffAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `WithTop` `ENat` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Nat.instAtLeastTwoHAddOfNat`	`Laplacian.laplacian` `InnerProductSpace.instLaplacian` `DFunLike.coe` `ContinuousLinearMap` `Real.semiring` `RingHom.id` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `ContinuousLinearMap.funLike`	—	`Nat.instAtLeastTwoHAddOfNat` `InnerProductSpace.laplacian_eq_iteratedFDeriv_stdOrthonormalBasis` `Finset.sum_congr` `ContinuousLinearMap.iteratedFDeriv_comp_left` `ContinuousLinearMap.compContinuousMultilinearMap_coe` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass`
`laplacian_CLM_comp_left_nhds` 📖	mathematical	`ContDiffAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `WithTop` `ENat` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Nat.instAtLeastTwoHAddOfNat`	`Filter.EventuallyEq` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Laplacian.laplacian` `InnerProductSpace.instLaplacian` `DFunLike.coe` `ContinuousLinearMap` `Real.semiring` `RingHom.id` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `ContinuousLinearMap.funLike`	—	`Nat.instAtLeastTwoHAddOfNat` `Filter.mp_mem` `eventually` `Filter.univ_mem'` `laplacian_CLM_comp_left`
`laplacian_add` 📖	mathematical	`ContDiffAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `WithTop` `ENat` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Nat.instAtLeastTwoHAddOfNat`	`Laplacian.laplacian` `InnerProductSpace.instLaplacian` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`Nat.instAtLeastTwoHAddOfNat` `InnerProductSpace.laplacian_eq_iteratedFDeriv_stdOrthonormalBasis` `Finset.sum_congr` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `iteratedFDeriv_add_apply`
`laplacian_add_nhds` 📖	mathematical	`ContDiffAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `WithTop` `ENat` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Nat.instAtLeastTwoHAddOfNat`	`Filter.EventuallyEq` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Laplacian.laplacian` `InnerProductSpace.instLaplacian` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`Nat.instAtLeastTwoHAddOfNat` `Filter.mp_mem` `eventually` `Filter.univ_mem'` `laplacian_add`

ContDiffWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`laplacianWithin_CLM_comp_left` 📖	mathematical	`ContDiffWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `WithTop` `ENat` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Nat.instAtLeastTwoHAddOfNat` `UniqueDiffOn` `Real.semiring` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set` `Set.instMembership`	`InnerProductSpace.laplacianWithin` `DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.funLike`	—	`Nat.instAtLeastTwoHAddOfNat` `InnerProductSpace.laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis` `Finset.sum_congr` `ContinuousLinearMap.iteratedFDerivWithin_comp_left` `ContinuousLinearMap.compContinuousMultilinearMap_coe` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass`
`laplacianWithin_CLM_comp_left_nhds` 📖	mathematical	`ContDiffWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `WithTop` `ENat` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Nat.instAtLeastTwoHAddOfNat` `UniqueDiffOn` `Real.semiring` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`Filter.EventuallyEq` `nhdsWithin` `InnerProductSpace.laplacianWithin` `DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.funLike`	—	`Nat.instAtLeastTwoHAddOfNat` `Filter.mp_mem` `eventually_mem_nhdsWithin` `Filter.Eventually.filter_mono` `nhdsWithin_mono` `Set.subset_insert` `eventually` `Filter.univ_mem'` `laplacianWithin_CLM_comp_left`
`laplacianWithin_add` 📖	mathematical	`ContDiffWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `WithTop` `ENat` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Nat.instAtLeastTwoHAddOfNat` `UniqueDiffOn` `Real.semiring` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set` `Set.instMembership`	`InnerProductSpace.laplacianWithin` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`Nat.instAtLeastTwoHAddOfNat` `InnerProductSpace.laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis` `Finset.sum_congr` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `iteratedFDerivWithin_add_apply`

InnerProductSpace

Definitions

Name	Category	Theorems
`instLaplacian` 📖	CompOp	14 math math: `ContDiffAt.laplacian_CLM_comp_left`, `ContDiffAt.laplacian_add`, `laplacian_smul`, `ContDiffAt.laplacian_add_nhds`, `laplacian_congr_nhds`, `laplacianWithin_univ`, `laplacian_eq_iteratedFDeriv_stdOrthonormalBasis`, `laplacian_eq_iteratedFDeriv_complexPlane`, `ContDiffAt.laplacian_CLM_comp_left_nhds`, `laplacian_eq_iteratedFDeriv_orthonormalBasis`, `laplacian_eq_iteratedDeriv_real`, `laplacian_smul_nhds`, `laplacian_CLE_comp_left`, `SchwartzMap.laplacian_apply`
`laplacianWithin` 📖	CompOp	13 math math: `ContDiffWithinAt.laplacianWithin_add`, `laplacianWithin_eq_iteratedFDerivWithin_complexPlane`, `laplacianWithin_smul`, `laplacianWithin_congr_nhdsWithin`, `laplacianWithin_eq_iteratedFDerivWithin_orthonormalBasis`, `ContDiffWithinAt.laplacianWithin_CLM_comp_left`, `laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis`, `ContDiffWithinAt.laplacianWithin_CLM_comp_left_nhds`, `laplacianWithin_eq_iteratedDerivWithin_real`, `laplacianWithin_univ`, `ContDiffAt.laplacianWithin_add_nhdsWithin`, `laplacianWithin_smul_nhds`, `laplacianWithin_CLE_comp_left`
`«termΔ[_]_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`laplacianWithin_CLE_comp_left` 📖	mathematical	`UniqueDiffOn` `Real` `Real.semiring` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `toNormedSpace` `Real.instRCLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set` `Set.instMembership`	`laplacianWithin` `DFunLike.coe` `ContinuousLinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike`	—	`RingHomInvPair.ids` `laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis` `Finset.sum_congr` `ContinuousLinearEquiv.iteratedFDerivWithin_comp_left` `ContinuousLinearMap.compContinuousMultilinearMap_coe` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousSemilinearEquivClass.continuousSemilinearMapClass` `ContinuousLinearEquiv.continuousSemilinearEquivClass`
`laplacianWithin_congr_nhdsWithin` 📖	mathematical	`Filter.EventuallyEq` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniqueDiffOn` `Real` `Real.semiring` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `toNormedSpace` `Real.instRCLike`	`laplacianWithin`	—	`Filter.mp_mem` `eventually_mem_nhdsWithin` `Filter.EventuallyEq.iteratedFDerivWithin` `Filter.univ_mem'` `laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis` `Finset.sum_congr`
`laplacianWithin_eq_iteratedDerivWithin_real` 📖	mathematical	`UniqueDiffOn` `Real` `Real.semiring` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Set` `Set.instMembership`	`laplacianWithin` `Real.normedAddCommGroup` `FiniteDimensional.rclike_to_real` `iteratedDerivWithin` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField`	—	`FiniteDimensional.rclike_to_real` `laplacianWithin_eq_iteratedFDerivWithin_orthonormalBasis` `Finset.sum_congr` `Finset.univ_unique` `OrthonormalBasis.singleton_apply` `Finset.sum_const` `Finset.card_singleton` `one_smul` `Fintype.complete` `Matrix.cons_val_fin_one`
`laplacianWithin_eq_iteratedFDerivWithin_complexPlane` 📖	mathematical	`UniqueDiffOn` `Real` `Complex` `Real.semiring` `Complex.addCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `toNormedSpace` `Real.instRCLike` `instInnerProductSpaceRealComplex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `Set` `Set.instMembership`	`laplacianWithin` `Complex.instNormedAddCommGroup` `FiniteDimensional.rclike_to_real` `Complex.instRCLike` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DFunLike.coe` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `ContinuousMultilinearMap.funLike` `iteratedFDerivWithin` `Matrix.vecCons` `Complex.instOne` `Matrix.vecEmpty` `Complex.I`	—	`FiniteDimensional.rclike_to_real` `laplacianWithin_eq_iteratedFDerivWithin_orthonormalBasis` `Finset.sum_congr` `Complex.coe_orthonormalBasisOneI` `Fin.sum_univ_two` `Matrix.cons_val_fin_one`
`laplacianWithin_eq_iteratedFDerivWithin_orthonormalBasis` 📖	mathematical	`UniqueDiffOn` `Real` `Real.semiring` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `toNormedSpace` `Real.instRCLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set` `Set.instMembership`	`laplacianWithin` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Finset.univ` `DFunLike.coe` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `ContinuousMultilinearMap.funLike` `iteratedFDerivWithin` `Matrix.vecCons` `OrthonormalBasis` `OrthonormalBasis.instFunLike` `Matrix.vecEmpty`	—	`canonicalCovariantTensor_eq_sum` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Finset.sum_congr` `tensorIteratedFDerivWithinTwo_eq_iteratedFDerivWithin`
`laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis` 📖	mathematical	`UniqueDiffOn` `Real` `Real.semiring` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `toNormedSpace` `Real.instRCLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set` `Set.instMembership`	`laplacianWithin` `Finset.sum` `Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Finset.univ` `Fin.fintype` `DFunLike.coe` `ContinuousMultilinearMap` `NontriviallyNormedField.toNormedField` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `ContinuousMultilinearMap.funLike` `iteratedFDerivWithin` `Matrix.vecCons` `OrthonormalBasis` `OrthonormalBasis.instFunLike` `stdOrthonormalBasis` `Matrix.vecEmpty`	—	`laplacianWithin_eq_iteratedFDerivWithin_orthonormalBasis`
`laplacianWithin_smul` 📖	mathematical	`ContDiffWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `WithTop` `ENat` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Nat.instAtLeastTwoHAddOfNat` `UniqueDiffOn` `Real.semiring` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set` `Set.instMembership`	`laplacianWithin` `Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid`	—	`Nat.instAtLeastTwoHAddOfNat` `laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis` `Finset.sum_congr` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `IsScalarTower.to_smulCommClass` `iteratedFDerivWithin_const_smul_apply` `Finset.smul_sum`
`laplacianWithin_smul_nhds` 📖	mathematical	`ContDiffWithinAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `WithTop` `ENat` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Nat.instAtLeastTwoHAddOfNat` `UniqueDiffOn` `Real.semiring` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`Filter.EventuallyEq` `nhdsWithin` `laplacianWithin` `Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid`	—	`Nat.instAtLeastTwoHAddOfNat` `Filter.mp_mem` `eventually_mem_nhdsWithin` `Filter.Eventually.filter_mono` `nhdsWithin_mono` `Set.subset_insert` `ContDiffWithinAt.eventually` `Filter.univ_mem'` `laplacianWithin_smul`
`laplacianWithin_univ` 📖	mathematical	—	`laplacianWithin` `Set.univ` `Laplacian.laplacian` `instLaplacian`	—	`smulCommClass_self` `fderivWithin_univ`
`laplacian_CLE_comp_left` 📖	mathematical	—	`Laplacian.laplacian` `instLaplacian` `DFunLike.coe` `ContinuousLinearEquiv` `Real` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike`	—	`RingHomInvPair.ids` `laplacian_eq_iteratedFDeriv_stdOrthonormalBasis` `Finset.sum_congr` `ContinuousLinearEquiv.iteratedFDeriv_comp_left` `ContinuousLinearMap.compContinuousMultilinearMap_coe` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousSemilinearEquivClass.continuousSemilinearMapClass` `ContinuousLinearEquiv.continuousSemilinearEquivClass`
`laplacian_congr_nhds` 📖	mathematical	`Filter.EventuallyEq` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`Laplacian.laplacian` `instLaplacian`	—	`Filter.mp_mem` `Filter.EventuallyEq.iteratedFDeriv` `Filter.univ_mem'` `laplacian_eq_iteratedFDeriv_stdOrthonormalBasis` `Finset.sum_congr`
`laplacian_eq_iteratedDeriv_real` 📖	mathematical	—	`Laplacian.laplacian` `instLaplacian` `Real` `Real.normedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Real.instRCLike` `FiniteDimensional.rclike_to_real` `iteratedDeriv` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField`	—	`FiniteDimensional.rclike_to_real` `laplacianWithin_univ` `iteratedDerivWithin_univ` `laplacianWithin_eq_iteratedDerivWithin_real` `Real.punctured_nhds_module_neBot` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Real.instNontrivial` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology`
`laplacian_eq_iteratedFDeriv_complexPlane` 📖	mathematical	—	`Laplacian.laplacian` `instLaplacian` `Complex` `Complex.instNormedAddCommGroup` `instInnerProductSpaceRealComplex` `FiniteDimensional.rclike_to_real` `Complex.instRCLike` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DFunLike.coe` `ContinuousMultilinearMap` `Real` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedSpace.toModule` `toNormedSpace` `Real.instRCLike` `ContinuousMultilinearMap.funLike` `iteratedFDeriv` `Matrix.vecCons` `Complex.instOne` `Matrix.vecEmpty` `Complex.I`	—	`FiniteDimensional.rclike_to_real` `laplacian_eq_iteratedFDeriv_orthonormalBasis` `Finset.sum_congr` `Complex.coe_orthonormalBasisOneI` `Fin.sum_univ_two` `Matrix.cons_val_fin_one`
`laplacian_eq_iteratedFDeriv_orthonormalBasis` 📖	mathematical	—	`Laplacian.laplacian` `instLaplacian` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Finset.univ` `DFunLike.coe` `ContinuousMultilinearMap` `Real` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedSpace.toModule` `toNormedSpace` `Real.instRCLike` `ContinuousMultilinearMap.funLike` `iteratedFDeriv` `Matrix.vecCons` `OrthonormalBasis` `OrthonormalBasis.instFunLike` `Matrix.vecEmpty`	—	`canonicalCovariantTensor_eq_sum` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Finset.sum_congr` `tensorIteratedFDerivTwo_eq_iteratedFDeriv`
`laplacian_eq_iteratedFDeriv_stdOrthonormalBasis` 📖	mathematical	—	`Laplacian.laplacian` `instLaplacian` `Finset.sum` `Module.finrank` `Real` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Real.instRCLike` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `toNormedSpace` `Finset.univ` `Fin.fintype` `DFunLike.coe` `ContinuousMultilinearMap` `NontriviallyNormedField.toNormedField` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `ContinuousMultilinearMap.funLike` `iteratedFDeriv` `Matrix.vecCons` `OrthonormalBasis` `OrthonormalBasis.instFunLike` `stdOrthonormalBasis` `Matrix.vecEmpty`	—	`laplacian_eq_iteratedFDeriv_orthonormalBasis`
`laplacian_smul` 📖	mathematical	`ContDiffAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `WithTop` `ENat` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Nat.instAtLeastTwoHAddOfNat`	`Laplacian.laplacian` `instLaplacian` `Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule`	—	`Nat.instAtLeastTwoHAddOfNat` `laplacian_eq_iteratedFDeriv_stdOrthonormalBasis` `Finset.sum_congr` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `IsScalarTower.to_smulCommClass` `iteratedFDeriv_const_smul_apply` `Finset.smul_sum`
`laplacian_smul_nhds` 📖	mathematical	`ContDiffAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `WithTop` `ENat` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `WithTop.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Nat.instAtLeastTwoHAddOfNat`	`Filter.EventuallyEq` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Laplacian.laplacian` `instLaplacian` `Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule`	—	`Nat.instAtLeastTwoHAddOfNat` `Filter.mp_mem` `ContDiffAt.eventually` `Filter.univ_mem'` `laplacian_smul`

InnerProductSpace.InnerProduct

Definitions

Name	Category	Theorems
`laplacian` 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
`Laplacian` 📖	CompData	—
`bilinearIteratedFDerivTwo` 📖	CompOp	1 math math: `bilinearIteratedFDerivTwo_eq_iteratedFDeriv`
`bilinearIteratedFDerivWithinTwo` 📖	CompOp	1 math math: `bilinearIteratedFDerivWithinTwo_eq_iteratedFDeriv`
`tensorIteratedFDerivTwo` 📖	CompOp	1 math math: `tensorIteratedFDerivTwo_eq_iteratedFDeriv`
`tensorIteratedFDerivWithinTwo` 📖	CompOp	1 math math: `tensorIteratedFDerivWithinTwo_eq_iteratedFDerivWithin`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bilinearIteratedFDerivTwo_eq_iteratedFDeriv` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `bilinearIteratedFDerivTwo` `ContinuousMultilinearMap` `ContinuousMultilinearMap.funLike` `iteratedFDeriv` `Matrix.vecCons` `Matrix.vecEmpty`	—	`IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `iteratedFDeriv_two_apply` `Matrix.cons_val_fin_one`
`bilinearIteratedFDerivWithinTwo_eq_iteratedFDeriv` 📖	mathematical	`UniqueDiffOn` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set` `Set.instMembership`	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `bilinearIteratedFDerivWithinTwo` `ContinuousMultilinearMap` `ContinuousMultilinearMap.funLike` `iteratedFDerivWithin` `Matrix.vecCons` `Matrix.vecEmpty`	—	`IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `iteratedFDerivWithin_two_apply` `Matrix.cons_val_fin_one`
`tensorIteratedFDerivTwo_eq_iteratedFDeriv` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `Semifield.toCommSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearMap.instFunLike` `tensorIteratedFDerivTwo` `TensorProduct.tmul` `ContinuousMultilinearMap` `ContinuousMultilinearMap.funLike` `iteratedFDeriv` `Matrix.vecCons` `Matrix.vecEmpty`	—	`smulCommClass_self` `bilinearIteratedFDerivTwo_eq_iteratedFDeriv` `tensorIteratedFDerivTwo.eq_1` `TensorProduct.lift.tmul`
`tensorIteratedFDerivWithinTwo_eq_iteratedFDerivWithin` 📖	mathematical	`UniqueDiffOn` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set` `Set.instMembership`	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `Semifield.toCommSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearMap.instFunLike` `tensorIteratedFDerivWithinTwo` `TensorProduct.tmul` `ContinuousMultilinearMap` `ContinuousMultilinearMap.funLike` `iteratedFDerivWithin` `Matrix.vecCons` `Matrix.vecEmpty`	—	`smulCommClass_self` `bilinearIteratedFDerivWithinTwo_eq_iteratedFDeriv` `tensorIteratedFDerivWithinTwo.eq_1` `TensorProduct.lift.tmul`

---

← Back to Index