dual_apply — Mathlib

English

For each g ∈ G, the action of g on the dual module is the transpose action: (dual ρ)V(g) = Module.Dual.transpose (ρ(g)^{-1}).

Русский

Для каждого g ∈ G действие на двойственном модуле реализуется через транспонирование: (dual ρ)V(g) = Module.Dual.transpose (ρ(g)^{-1}).

LaTeX

$$$ (dual ρ) g = \\mathrm{Module.Dual.transpose} (\\rho g^{-1}) $$$

Lean4

@[simp]
theorem dual_apply (g : G) : (dual ρV) g = Module.Dual.transpose (R := k) (ρV g⁻¹) :=
  rfl

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