congr_pow — Mathlib

English

For integer exponent n, congr f g raised to n equals congr(f^n)(g^n): congr f g)^n = congr(f^n) (g^n).

Русский

Для целочисленного показателя n выполняется (congr f g)^n = congr(f^n) (g^n).

LaTeX

$$$ congr\\ f\\ g\\ ^{n} = congr\\ (f^{n})\\ (g^{n}) $$$

Lean4

@[simp]
theorem congr_pow (f : M ≃ₗ[R] M) (g : N ≃ₗ[R] N) (n : ℕ) : congr f g ^ n = congr (f ^ n) (g ^ n) := by
  induction n with
  | zero => exact congr_refl_refl.symm
  | succ n ih => simp_rw [pow_succ, ih, congr_mul]

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