instGroup — Mathlib

English

If β is a group, then the collection of simple functions α →ₛ β forms a group under pointwise operations.

Русский

Если β — группа, то множество простых функций α →ₛ β образует группу под покоятельскими операциями по точкам.

LaTeX

$$$\\text{instGroup }[Group\\;\\beta]:\\;\\text{Group}(\\alpha \\to_{S} \\beta).$$$

Lean4

@[to_additive existing]
instance instGroup [Group β] : Group (α →ₛ β) :=
  fast_instance%Function.Injective.group (fun f => show α → β from f) coe_injective coe_one coe_mul coe_inv coe_div
      coe_pow coe_zpow

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