mulAutArrow — Mathlib

English

Given groups G and H with G acting on A, G acts by multiplicative automorphisms on the function space A → H, yielding a hom mulAutArrow: G →* MulAut (A → H).

Русский

Даны группы G и H с действием G на A; G действует как множностный автоморфизм на множество функций A → H, образуя моноид-гомоморфизм mulAutArrow: G →* MulAut (A → H).

LaTeX

$$$\text{mulAutArrow} : G \to_* \mathrm{MulAut}(A \to M).$$$

Lean4

/-- Given groups `G H` with `G` acting on `A`, `G` acts by
multiplicative automorphisms on `A → H`. -/
@[simps!]
def mulAutArrow : G →* MulAut (A → M) :=
  MulDistribMulAction.toMulAut _ _

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