pow_mulLeft — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem pow_mulLeft (a : A) (n : ℕ) : mulLeft R a ^ n = mulLeft R (a ^ n) :=
  match n with
  | 0 => by rw [pow_zero, pow_zero, mulLeft_one, Module.End.one_eq_id]
  | (n + 1) => by rw [pow_succ, pow_succ, mulLeft_mul, Module.End.mul_eq_comp, pow_mulLeft]

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