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, laplacianWithin_sub_nhdsWithin, laplacian_CLM_comp_left, laplacian_CLM_comp_left_nhds, laplacian_add, laplacian_add_nhds, laplacian_sub, laplacian_sub_nhds, laplacianWithin_CLM_comp_left, laplacianWithin_CLM_comp_left_nhds, laplacianWithin_add, laplacianWithin_sub, laplacianWithin_CLE_comp_left, laplacianWithin_congr_nhdsWithin, laplacianWithin_eq_iteratedDerivWithin_real, laplacianWithin_eq_iteratedFDerivWithin_complexPlane, laplacianWithin_eq_iteratedFDerivWithin_orthonormalBasis, laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis, laplacianWithin_neg, laplacianWithin_smul, laplacianWithin_smul_nhds, laplacianWithin_univ, laplacian_CLE_comp_left, laplacian_congr_nhds, laplacian_const, laplacian_eq_iteratedDeriv_real, laplacian_eq_iteratedFDeriv_complexPlane, laplacian_eq_iteratedFDeriv_orthonormalBasis, laplacian_eq_iteratedFDeriv_stdOrthonormalBasis, laplacian_neg, laplacian_smul, laplacian_smul_nhds, bilinearIteratedFDerivTwo_eq_iteratedFDeriv, bilinearIteratedFDerivWithinTwo_eq_iteratedFDeriv, tensorIteratedFDerivTwo_eq_iteratedFDeriv, tensorIteratedFDerivWithinTwo_eq_iteratedFDerivWithin	36
Total	45

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 WithTop.natCast ENat.instNatCast Nat.instAtLeastTwoHAddOfNat UniqueDiffOn Real.semiring NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Set Set.instMembership	Filter.EventuallyEq nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup 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
laplacianWithin_sub_nhdsWithin 📖	mathematical	ContDiffWithinAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup WithTop ENat instOfNatAtLeastTwo WithTop.natCast ENat.instNatCast Nat.instAtLeastTwoHAddOfNat UniqueDiffOn Real.semiring NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Set Set.instMembership	Filter.EventuallyEq nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.laplacianWithin Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	Nat.instAtLeastTwoHAddOfNat Set.insert_eq_of_mem Filter.mp_mem eventually_mem_nhdsWithin ContDiffWithinAt.eventually Filter.univ_mem' ContDiffWithinAt.laplacianWithin_sub
laplacian_CLM_comp_left 📖	mathematical	ContDiffAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup WithTop ENat instOfNatAtLeastTwo WithTop.natCast ENat.instNatCast Nat.instAtLeastTwoHAddOfNat	Laplacian.laplacian InnerProductSpace.instLaplacian DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup 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 instReflLe 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 WithTop.natCast ENat.instNatCast Nat.instAtLeastTwoHAddOfNat	Filter.EventuallyEq nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Laplacian.laplacian InnerProductSpace.instLaplacian DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring 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 WithTop.natCast ENat.instNatCast Nat.instAtLeastTwoHAddOfNat	Laplacian.laplacian InnerProductSpace.instLaplacian Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup 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 WithTop.natCast ENat.instNatCast Nat.instAtLeastTwoHAddOfNat	Filter.EventuallyEq nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup 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
laplacian_sub 📖	mathematical	ContDiffAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup WithTop ENat instOfNatAtLeastTwo WithTop.natCast ENat.instNatCast Nat.instAtLeastTwoHAddOfNat	Laplacian.laplacian InnerProductSpace.instLaplacian Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	Nat.instAtLeastTwoHAddOfNat InnerProductSpace.laplacian_eq_iteratedFDeriv_stdOrthonormalBasis Finset.sum_congr SeminormedAddCommGroup.toIsTopologicalAddGroup iteratedFDeriv_sub_apply
laplacian_sub_nhds 📖	mathematical	ContDiffAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup WithTop ENat instOfNatAtLeastTwo WithTop.natCast ENat.instNatCast Nat.instAtLeastTwoHAddOfNat	Filter.EventuallyEq nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Laplacian.laplacian InnerProductSpace.instLaplacian Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	Nat.instAtLeastTwoHAddOfNat Filter.mp_mem eventually Filter.univ_mem' laplacian_sub

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 WithTop.natCast ENat.instNatCast 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 Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.funLike	—	Nat.instAtLeastTwoHAddOfNat InnerProductSpace.laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis Finset.sum_congr ContinuousLinearMap.iteratedFDerivWithin_comp_left instReflLe 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 WithTop.natCast ENat.instNatCast Nat.instAtLeastTwoHAddOfNat UniqueDiffOn Real.semiring NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	Filter.EventuallyEq nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.laplacianWithin DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField 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 WithTop.natCast ENat.instNatCast 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 UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	Nat.instAtLeastTwoHAddOfNat InnerProductSpace.laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis Finset.sum_congr IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup iteratedFDerivWithin_add_apply
laplacianWithin_sub 📖	mathematical	ContDiffWithinAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup WithTop ENat instOfNatAtLeastTwo WithTop.natCast ENat.instNatCast Nat.instAtLeastTwoHAddOfNat UniqueDiffOn Real.semiring NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Set Set.instMembership	InnerProductSpace.laplacianWithin Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	Nat.instAtLeastTwoHAddOfNat InnerProductSpace.laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis Finset.sum_congr SeminormedAddCommGroup.toIsTopologicalAddGroup iteratedFDerivWithin_sub_apply

InnerProductSpace

Definitions

Name	Category	Theorems
instLaplacian 📖	CompOp	18 math math: ContDiffAt.laplacian_CLM_comp_left, ContDiffAt.laplacian_add, laplacian_smul, ContDiffAt.laplacian_sub, 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_neg, laplacian_eq_iteratedDeriv_real, laplacian_smul_nhds, laplacian_CLE_comp_left, SchwartzMap.laplacian_apply, ContDiffAt.laplacian_sub_nhds, laplacian_const
laplacianWithin 📖	CompOp	16 math math: ContDiffWithinAt.laplacianWithin_sub, ContDiffWithinAt.laplacianWithin_add, laplacianWithin_eq_iteratedFDerivWithin_complexPlane, laplacianWithin_smul, laplacianWithin_neg, 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, ContDiffAt.laplacianWithin_sub_nhdsWithin, 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 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 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	Filter.EventuallyEq nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup 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 Real.normedAddCommGroup RCLike.toInnerProductSpaceReal Real.instRCLike 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 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 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 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 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 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 iteratedFDerivWithin Matrix.vecCons OrthonormalBasis OrthonormalBasis.instFunLike stdOrthonormalBasis Matrix.vecEmpty	—	laplacianWithin_eq_iteratedFDerivWithin_orthonormalBasis
laplacianWithin_neg 📖	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 Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis SeminormedAddCommGroup.toIsTopologicalAddGroup iteratedFDerivWithin_neg_apply Finset.sum_congr Finset.sum_neg_distrib
laplacianWithin_smul 📖	mathematical	ContDiffWithinAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup WithTop ENat instOfNatAtLeastTwo WithTop.natCast ENat.instNatCast 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 UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup 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 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 WithTop.natCast ENat.instNatCast Nat.instAtLeastTwoHAddOfNat UniqueDiffOn Real.semiring NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	Filter.EventuallyEq nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup 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 NormedSpace.toModule	—	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	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_const 📖	mathematical	—	Laplacian.laplacian instLaplacian Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	laplacian_eq_iteratedFDeriv_stdOrthonormalBasis Finset.sum_congr iteratedFDeriv_const_of_ne two_ne_zero Finset.sum_const_zero
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 IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal Real.instNontrivial IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring
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_neg 📖	mathematical	—	Laplacian.laplacian instLaplacian Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	SeminormedAddCommGroup.toIsTopologicalAddGroup laplacian_eq_iteratedFDeriv_stdOrthonormalBasis Finset.sum_congr iteratedFDeriv_neg Finset.sum_neg_distrib
laplacian_smul 📖	mathematical	ContDiffAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup WithTop ENat instOfNatAtLeastTwo WithTop.natCast ENat.instNatCast Nat.instAtLeastTwoHAddOfNat	Laplacian.laplacian instLaplacian Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup 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 WithTop.natCast ENat.instNatCast Nat.instAtLeastTwoHAddOfNat	Filter.EventuallyEq nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup 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 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 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 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 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