coe_pow — Mathlib

English

For SubMulAction p, the power p^n coerces to the nth NPow of the underlying set, with the standard behavior for n = 0 and n = 1.

Русский

Для SubMulAction p отображение p^n коэрцируется к n-й NPow подмножества, с обычным поведением для n=0 и n=1.

LaTeX

$$$\\forall p : \\mathrm{SubMulAction} \\ R M, \\forall n, n \\neq 0 \\implies \\uparrow(p^{n}) = (\\uparrow p)^{n}.$$$

Lean4

theorem coe_pow (p : SubMulAction R M) : ∀ {n : ℕ} (_ : n ≠ 0), ↑(p ^ n) = (p : Set M) ^ n
  | 0, hn => (hn rfl).elim
  | 1, _ => by rw [pow_one, pow_one]
  | n + 2, _ => by rw [pow_succ _ (n + 1), pow_succ _ (n + 1), coe_mul, coe_pow _ n.succ_ne_zero]

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