pow_pow — Mathlib

English

If a is associated with b, then a^n is associated with b^n for all natural n.

Русский

Если a ассоциировано с b, то a^n ассоциировано с b^n для всех натуральных n.

LaTeX

$$$ [CommMonoid M] {a b : M} {n : \mathbb{N}} (h : a ~ᵤ b) : a ^ n ~ᵤ b ^ n $$$

Lean4

theorem pow_pow [CommMonoid M] {a b : M} {n : ℕ} (h : a ~ᵤ b) : a ^ n ~ᵤ b ^ n := by
  induction n with
  | zero => simp [Associated.refl]
  | succ n ih => convert h.mul_mul ih <;> rw [pow_succ']

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