domCongr_apply — Mathlib

English

For e ∈ G ≃* H and f ∈ MonoidAlgebra A G and h ∈ H, the action of domCongr on f at h equals f applied to e.symm(h): domCongr k A e f h = f(e.symm h).

Русский

Для e ∈ G ≃* H и f ∈ MonoidAlgebra A G и h ∈ H верно: domCongr k A e f h = f(e.symm h).

LaTeX

$$$\\mathrm{domCongr}\\ k\\;A\\;e\\;f\\;h = f\\big(e^{-1}(h)\\big).$$$

Lean4

@[to_additive (attr := simp)]
theorem domCongr_apply (e : G ≃* H) (f : MonoidAlgebra A G) (h : H) : domCongr k A e f h = f (e.symm h) :=
  rfl

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