pow_mulRight — Mathlib

English

Powers of right multiplication correspond to right multiplication by powers: mulRight R a^n = mulRight R (a^n).

Русский

Степени правого умножения соответствуют правому умножению на степени: mulRight R a^n = mulRight R (a^n).

LaTeX

$$$$ mulRight R a^n = mulRight R (a^n). $$$$

Lean4

@[simp]
theorem pow_mulRight (a : A) (n : ℕ) : mulRight R a ^ n = mulRight R (a ^ n) :=
  match n with
  | 0 => by rw [pow_zero, pow_zero, mulRight_one, Module.End.one_eq_id]
  | (n + 1) => by rw [pow_succ, pow_succ', mulRight_mul, Module.End.mul_eq_comp, pow_mulRight]

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