Theorems · Theorem · difference equations
fwdDiff_iter_const_smul
∀ {M : Type u_1} {G : Type u_2} [inst : AddCommMonoid M] [inst_1 : AddCommGroup G] (h : M) {R : Type u_3}
[inst_2 : Monoid R] [inst_3 : DistribMulAction R G] (r : R) (f : M → G) (n : ℕ),
(fwdDiff h)^[n] (r • f) = r • (fwdDiff h)^[n] f- Defined in
- Mathlib.Algebra.Group.ForwardDiff
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 15 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddCommGroupstatement and proof · cited by 12,871
- AddCommMonoidstatement and proof · cited by 12,281
- Monoidstatement and proof · cited by 3,887
- Nat.iteratestatement and proof · cited by 740
- DistribMulActionstatement and proof · cited by 584
- fwdDiffstatement and proof · cited by 35
- fwdDiff_const_smulproof · cited by 1
Cited by4
Results whose statement or proof uses this declaration.
- fwdDiff_iter_pow_eq_zero_of_ltproof · cited by 3
- fwdDiff_iter_eq_factorialproof · cited by 1
- Polynomial.fwdDiff_iter_degree_eq_factorialproof · cited by 1
- fwdDiff_iter_sum_mul_pow_eq_zeroproof · cited by 0