eval₂_T — Mathlib

English

For any integer n, eval₂ f x (T^n) equals (x^n).val, the value in S.

Русский

Для любого целого n: eval₂ f x (T^n) равно (x^n).val, т.е. значение в S.

LaTeX

$$$\\mathrm{eval_2}(f,x)(T^{n}) = (x^{n}).\\text{val}$ for $n \\in \\mathbb{Z}$.$$

Lean4

@[simp]
theorem eval₂_T (n : ℤ) : eval₂ f x (T n) = (x ^ n).val :=
  by
  by_cases hn : 0 ≤ n
  · lift n to ℕ using hn
    apply eval₂_T_n
  · obtain ⟨m, rfl⟩ := Int.exists_eq_neg_ofNat (Int.le_of_not_le hn)
    rw [eval₂_T_neg_n, zpow_neg, zpow_natCast, ← inv_pow, Units.val_pow_eq_pow_val]

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