pow_apply_coe — Mathlib

English

If χ is a multiplicative character and a is a unit, then (χ^n)(a) = (χ(a))^n for any n ∈ ℕ.

Русский

Если χ — мультипликативный характер, и a — единица, то (χ^n)(a) = (χ(a))^n для любого n ∈ ℕ.

LaTeX

$$$$ (\\chi^n)(a) = (\\chi(a))^n \\quad (a \\in R^\\times). $$$$

Lean4

/-- If `a` is a unit and `n : ℕ`, then `(χ ^ n) a = (χ a) ^ n`. -/
theorem pow_apply_coe (χ : MulChar R R') (n : ℕ) (a : Rˣ) : (χ ^ n) a = χ a ^ n := by
  induction n with
  | zero => rw [pow_zero, pow_zero, one_apply_coe]
  | succ n ih => rw [pow_succ, pow_succ, mul_apply, ih]

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