map_pow — Mathlib

English

The map induced on tensor products respects powers: applying the map to powers i^n and j^n is the nth power of the induced map.

Русский

Полученное отображение на тензорном произведении сохраняет степени: отображение к степенным множителям i^n и j^n равно n-й степени от соответствующего отображения.

LaTeX

$$$ hf.map hf i j^n = (hf.map hf i^n j^n)$$$

Lean4

protected theorem map_pow (i : M₁ →ₗ[R] M₁) (j : M₂ →ₗ[R] M₂) (n : ℕ) : hf.map hf i j ^ n = hf.map hf (i ^ n) (j ^ n) :=
  by
  induction n with
  | zero => simp
  | succ n ih => simp only [pow_succ, ih, hf.map_mul]

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