English
If V and W are finite-dimensional representations, the scaled average of the product of their characters equals the dimension of Hom_G(V,W) in the given setting.
Русский
Для двух конечномерных представлений характеристическое среднее произведения равно размерности Hom_G(V,W).
LaTeX
$$$\frac{1}{|G|} \sum_{g \in G} W.\chi(g) \cdot V.\chi(g)^{-1} = \dim_k(\mathrm{Hom}_G(V,W)).$$$
Lean4
/-- If `ρ : Representation k G A` and `φ : G →* H` then `coindV φ ρ` is the sub-`k`-module of
functions `H → A` underlying the coinduction of `ρ` along `φ`, i.e., the functions `f : H → A`
such that `f (φ g * h) = (ρ g) (f h)` for all `g : G` and `h : H`.
-/
@[simps]
def coindV : Submodule k (H → A)
where
carrier := {f : H → A | ∀ (g : G) (h : H), f (φ g * h) = ρ g (f h)}
add_mem' _ _ _ _ := by simp_all
zero_mem' := by simp
smul_mem' _ _ _ := by simp_all
