Theorem HasFDerivAt.norm_sq

Modification history

2023-07-26 09:26

Mathlib/Analysis/InnerProductSpace/Calculus.lean

feat: derivative of the inversion (#5937) …

Added HasFDerivAt.norm_sq View on Github →