parabolicFixedPoint_pow — Mathlib

English

For a parabolic g, and any nonzero c ∈ OnePoint(K), g • c = c if and only if c = parabolicFixedPoint(g).

Русский

Для параболического g и любого не нулевого c ∈ OnePoint(K) верно: g • c = c тогда и только тогда, когда c = parabolicFixedPoint(g).

LaTeX

$$$g$ IsParabolic $\\Rightarrow$ $g \\cdot c = c \\iff c = parabolicFixedPoint(g)$ for all $c$.$$

Lean4

theorem parabolicFixedPoint_pow {g : GL (Fin 2) K} (hg : IsParabolic g) [CharZero K] {n : ℕ} (hn : n ≠ 0) :
    (g ^ n).parabolicFixedPoint = g.parabolicFixedPoint :=
  by
  rw [eq_comm, ← IsParabolic.smul_eq_self_iff (hg.pow hn)]
  clear hn
  induction n with
  | zero => simp
  | succ n IH => rw [pow_succ, MulAction.mul_smul, hg.smul_eq_self_iff.mpr rfl, IH]

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