mul_apply_right — Mathlib

English

Dual to the left-apply formula: (x * y) g = ∑_{h} y(h) · x(g · h⁻¹).

Русский

Двойственный к левой формуле вид: (x * y) g = ∑_{h} y(h) · x(g · h⁻¹).

LaTeX

$$$\\forall x,y \\in \\mathrm{MonoidAlgebra}(R,G),\\forall g\\in G,\\ (x*y)(g) = \\sum_{h\\in G} y(h) \\cdot x(g \\cdot h^{-1}).$$$

Lean4

@[to_additive (dont_translate := R) mul_apply_right]
theorem mul_apply_right (x y : MonoidAlgebra R G) (g : G) : (x * y) g = y.sum fun h r ↦ x (g * h⁻¹) * r := by
  classical
  rw [mul_apply, Finsupp.sum_comm]
  dsimp [Finsupp.sum]
  congr! 1
  simp +contextual [← eq_mul_inv_iff_mul_eq]

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