charpoly — Mathlib

English

For a finite group G acting on a ring B, the characteristic polynomial of the action is the product over G of (X − i·b) for i the action by g.

Русский

Для конечной группы G, действующей на кольцо B, характеристический многочлен действия равен произведению по G от (X − g·b).

LaTeX

$$$\text{charpoly}(b) = \prod_{g\in G} (X - (g\cdot b))$ in B[X].$$

Lean4

/-- Characteristic polynomial of a finite group action on a ring. -/
noncomputable def charpoly (b : B) : B[X] :=
  ∏ g : G, (X - C (g • b))

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