mem_invtSubmodule — Mathlib

English

A given submodule p ⊆ V lies in Inv(ρ) iff p lies in Inv(ρ(g)) for every g ∈ G; equivalently, p is invariant under all ρ(g).

Русский

Дано подполье p ⊆ V принадлежит Inv(ρ) тогда и только тогда, когда оно инвариантно относительно каждого ρ(g).

LaTeX

$$$p \\in \\rho.invtSubmodule \\iff \\forall g,\\ p \\in \\Module.End.invtSubmodule(\\rho(g)).$$$

Lean4

theorem mem_invtSubmodule {p : Submodule k V} : p ∈ ρ.invtSubmodule ↔ ∀ g, p ∈ Module.End.invtSubmodule (ρ g) := by
  rw [invtSubmodule, Sublattice.mem_iInf]

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