pow — Mathlib

English

If T is symmetric, then T^n is symmetric for all n ∈ ℕ.

Русский

Если T симметричен, то T^n симметричен для любого n ∈ ℕ.

LaTeX

$$$ (T^n).IsSymmetric$ for all $n \in \mathbb{N}$$$

Lean4

@[aesop safe apply]
theorem pow {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (n : ℕ) : (T ^ n).IsSymmetric :=
  by
  refine Nat.le_induction (by simp [Module.End.one_eq_id]) (fun k _ ih ↦ ?_) n n.zero_le
  rw [Module.End.iterate_succ, ← Module.End.mul_eq_comp]
  exact ih.mul_of_commute hT <| .pow_left rfl k

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