pow_apply' — Mathlib

English

If n ≠ 0, then (χ^n) a = χ(a)^n for all a ∈ R.

Русский

Если n ≠ 0, то (χ^n)(a) = χ(a)^n для всех a ∈ R.

LaTeX

$$$$ (\\chi^n) a = (\\chi(a))^n \\quad \\text{if } n \\neq 0. $$$$

Lean4

/-- If `n` is positive, then `(χ ^ n) a = (χ a) ^ n`. -/
theorem pow_apply' (χ : MulChar R R') {n : ℕ} (hn : n ≠ 0) (a : R) : (χ ^ n) a = χ a ^ n :=
  by
  by_cases ha : IsUnit a
  · exact pow_apply_coe χ n ha.unit
  · rw [map_nonunit (χ ^ n) ha, map_nonunit χ ha, zero_pow hn]

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