sub_mem_ker — Mathlib

English

For any g ∈ G and x ∈ V, the element ρ(g)x − x lies in the kernel of ρ when viewed in the coinvariants.

Русский

Для любого g ∈ G и x ∈ V элемент ρ(g)x − x принадлежит ядру отображения в коинвариантах.

LaTeX

$$$\rho(g)\,x - x \in \ker(\rho)$ (in the coinvariants)$$

Lean4

theorem sub_mem_ker (g : G) (x : V) : ρ g x - x ∈ Coinvariants.ker ρ :=
  Submodule.subset_span <| Set.mem_range_self (g, x)

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