mem_invariants — Mathlib

English

An element v lies in invariants ρ if and only if ρ(g) v = v for all g ∈ G.

Русский

Элемент v лежит в подпространстве инвариантов ρ тогда и только тогда, когда ρ(g) v = v для всех g ∈ G.

LaTeX

$$$$ v \in \mathrm{invariants}\;\rho \quad\Leftrightarrow\quad \forall g \in G,\; \rho(g)v = v. $$$$

Lean4

@[simp]
theorem mem_invariants (v : V) : v ∈ invariants ρ ↔ ∀ g : G, ρ g v = v := by rfl

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