Theorems · Theorem · real analysis
deriv.star
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] [inst_1 : StarRing 𝕜] {F : Type v} [inst_2 : NormedAddCommGroup F]
[inst_3 : NormedSpace 𝕜 F] [inst_4 : StarAddMonoid F] [StarModule 𝕜 F] [ContinuousStar F] {f : 𝕜 → F} {x : 𝕜}
[TrivialStar 𝕜], deriv (fun y => star (f y)) x = star (deriv f x)- Defined in
- Mathlib.Analysis.Calculus.Deriv.Star
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 175 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.
- NormedAddCommGroupstatement and proof · cited by 15,752
- NormedSpacestatement and proof · cited by 12,499
- NontriviallyNormedFieldstatement and proof · cited by 8,742
- StarRingstatement and proof · cited by 1,686
- Star.starstatement · cited by 1,082
- derivstatement · cited by 676
- StarModulestatement and proof · cited by 570
- ContinuousStarstatement and proof · cited by 543
- StarAddMonoidstatement and proof · cited by 296
- DFunLike.congr_funproof · cited by 288
- TrivialStarstatement and proof · cited by 66
- fderiv_starproof · cited by 1
Cited by1
Results whose statement or proof uses this declaration.
- deriv.star'proof · cited by 0