Theorems · Definition · real analysis
fderivPolarCoordSymm
ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ
The derivative of polarCoord.symm, see hasFDerivAt_polarCoord_symm.
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 171 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Realstatement and proof · cited by 25,697
- RingHom.idstatement · cited by 18,349
- ContinuousLinearMapstatement · cited by 5,352
- Matrix.vecConsproof · cited by 852
- Matrix.vecEmptyproof · cited by 832
- Real.cosproof · cited by 424
- Real.sinproof · cited by 389
- Matrix.ofproof · cited by 336
- Matrix.toLinproof · cited by 77
- LinearMap.toContinuousLinearMapproof · cited by 43
- Module.Basis.finTwoProdproof · cited by 7
Cited by5
Results whose statement or proof uses this declaration.
- fderivPiPolarCoordSymmproof · cited by 5
- det_fderivPolarCoordSymmstatement and proof · cited by 3
- hasFDerivAt_polarCoord_symmstatement · cited by 3
- det_fderivPiPolarCoordSymmproof · cited by 3
- integral_comp_polarCoord_symmproof · cited by 2