Mathlib Map

Theorems · Definition · global analysis

fderivInnerCLM

(𝕜 : Type u_1) →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup E] → [InnerProductSpace 𝕜 E] → [inst_3 : NormedSpace ℝ E] → E × E → E × E →L[ℝ] 𝕜

Derivative of the inner product.

Defined in
Mathlib.Analysis.InnerProductSpace.Calculus
Cited by
8 results in Mathlib
Foundations
Depth 180 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
RCLikeNormedAddCommGroupInnerProductSpaceNormedSpace
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

hasStrictFDerivAt_norm_sq · cited by 6hasStrictFDerivAt_norm_sqHasStrictFDerivAt.inner · cited by 2HasStrictFDerivAt.innerHasFDerivAt.inner · cited by 2HasFDerivAt.innerHasFDerivWithinAt.inner · cited by 2HasFDerivWithinAt.innerfderivInnerCLM_apply · cited by 1fderivInnerCLM_applyLinearMap.IsSymmetric.hasStrictFDerivAt_reApplyInnerSelf · cited by 1IsSymmetric.hasStrictFDer…HasDerivWithinAt.inner · cited by 1HasDerivWithinAt.innerfderiv_inner_apply · cited by 0fderiv_inner_applyReal · cited by 25697RealRingHom.id · cited by 18349RingHom.idNormedAddCommGroup · cited by 15752NormedAddCommGroupNormedSpace · cited by 12499NormedSpaceContinuousLinearMap · cited by 5352ContinuousLinearMapInnerProductSpace · cited by 3523InnerProductSpaceRCLike · cited by 2829RCLikeIsBoundedBilinearMap.deriv · cited by 8IsBoundedBilinearMap.derivfderivInnerCLMCITED BYCITES

Cites8

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by8

Results whose statement or proof uses this declaration.