fixpointPolynomial — Mathlib

English

For g ∈ GL(2,R), the fixed-point polynomial p_g(X) has roots equal to the fixed points of the Möbius transformation associated to g. In particular, p_g encodes fixed points of g.

Русский

Для g ∈ GL(2,R) фиксpoint-полином p_g(X) имеет корни, соответствующие фиксированным точкам соответствующего преобразования Мёбиуса.

LaTeX

$$$\text{fixpointPolynomial}(g) = C(g_{10}) X^2 + C(g_{11}-g_{00}) X - C(g_{01})$$$

Lean4

/-- Polynomial whose roots are the fixed points of `g` considered as a Möbius transformation.

See `Matrix.GeneralLinearGroup.fixpointPolynomial_aeval_eq_zero_iff`. -/
noncomputable def fixpointPolynomial (g : GL (Fin 2) R) : R[X] :=
  C (g 1 0) * X ^ 2 + C (g 1 1 - g 0 0) * X - C (g 0 1)

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