Theorems · Theorem · global analysis

hasFDerivAt_stereoInvFunAux

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] (v : E),
  HasFDerivAt (stereoInvFunAux v) (ContinuousLinearMap.id ℝ E) 0

Defined in

Mathlib.Geometry.Manifold.Instances.Sphere

Cited by

1 results in Mathlib

Foundations

Depth 183 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupInnerProductSpace