conjugate_i — Mathlib

English

If there is a linear map i: V → W with π ∘ i = id_V, then for every g ∈ G and v ∈ V, the g-conjugate of π applied to i(v) yields v; i.e., (conjugate π g)(i(v)) = v.

Русский

Пусть π: W → V, i: V → W с π ∘ i = id_V. Тогда для любого g ∈ G и v ∈ V выполняется (π^g)(i(v)) = v.

LaTeX

$$$\forall g \in G, (\pi^{g})(i(v)) = v$$$

Lean4

theorem conjugate_i (h : ∀ v : V, π (i v) = v) (g : G) (v : V) : (conjugate π g : W → V) (i v) = v := by
  rw [conjugate_apply, ← i.map_smul, h, ← mul_smul, single_mul_single, mul_one, inv_mul_cancel, ← one_def, one_smul]

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