snd_pow — Mathlib

English

If R acts centrally on M, then for any x in tsze.R M and any n, snd(x^n) = n • fst(x)^n-1 • x.snd.

Русский

Если действие R на M центрально, тогда snd(x^n) = n · fst(x)^{n-1} · x.snd.

LaTeX

$$$\\\\mathrm{snd}(x^n) = n \\\\cdot (\\\\operatorname fst(x))^{n-1} \\\\cdot x.snd$$$

Lean4

@[simp]
theorem snd_pow [CommMonoid R] [AddMonoid M] [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] [IsCentralScalar R M]
    (x : tsze R M) (n : ℕ) : snd (x ^ n) = n • x.fst ^ n.pred • x.snd :=
  snd_pow_of_smul_comm _ _ (op_smul_eq_smul _ _)

Похожие утверждения