Theorems · Theorem · differential geometry

conformalFactorAt_inner_eq_mul_inner

∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : InnerProductSpace ℝ F] {f : E → F} {x : E} {f' : E →L[ℝ] F},
  HasFDerivAt f f' x → ∀ (H : ConformalAt f x) (u v : E), inner ℝ (f' u) (f' v) = conformalFactorAt H * inner ℝ u v

Defined in

Mathlib.Analysis.Calculus.Conformal.InnerProduct

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedAddCommGroupInnerProductSpaceInnerProductSpace