invariants_eq_inter — Mathlib

English

The carrier of invariants ρ equals the intersection, over all g ∈ G, of the fixed-point subspaces Fix(ρ(g)).

Русский

Множество инвариантов ρ равно пересечению всех подпространств фиксации Fix(ρ(g)) по всем g ∈ G.

LaTeX

$$$$ (\mathrm{invariants}\;\rho).\mathrm{carrier} = \bigcap_{g \in G} \mathrm{Fix}(\rho(g)). $$$$

Lean4

theorem invariants_eq_inter : (invariants ρ).carrier = ⋂ g : G, Function.fixedPoints (ρ g) := by ext;
  simp [Function.IsFixedPt]

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