spanSingleton_pow — Mathlib

English

Raising a span singleton to a natural power corresponds to taking the span singleton of the power.

Русский

Возведение spanSingleton в натуральную степень соответствует spanSingleton от степени.

LaTeX

$$$spanSingleton\\;S\\;x^n = (spanSingleton\\;S\\;x)^n$$$

Lean4

@[simp]
theorem spanSingleton_pow (x : P) (n : ℕ) : spanSingleton S x ^ n = spanSingleton S (x ^ n) := by
  induction n with
  | zero => rw [pow_zero, pow_zero, spanSingleton_one]
  | succ n hn => rw [pow_succ, hn, spanSingleton_mul_spanSingleton, pow_succ]

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