pow_mulShift — Mathlib

English

The n-th power of ψ equals mulShift ψ n cast, i.e., ψ^n = mulShift ψ n.cast.

Русский

Степень n характерa ψ равна mulShift ψ n.cast; то есть ψ^n = mulShift ψ n.cast.

LaTeX

$$$$\psi^{n} = \operatorname{mulShift}(\psi, n.{\tt cast}).$$$$

Lean4

/-- If `n` is a natural number, then `ψ ^ n = mulShift ψ n`. -/
theorem pow_mulShift (ψ : AddChar R M) (n : ℕ) : ψ ^ n = mulShift ψ n :=
  by
  ext x
  rw [pow_apply, ← mulShift_spec']

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