instMulAction — Mathlib

English

There is a multiplicative action of a group G on AffineBasis ι k V given by a • b, defined by (a • b)(i) = a • b(i).

Русский

Существует действие группы G на AffineBasis ι k V: (a • b)(i) = a • b(i).

LaTeX

$$$ (a \\cdot b)(i) = a \\cdot b(i)$$$

Lean4

/-- TODO: generalize to include `SMul (P ≃ᵃ[k] P) (AffineBasis ι k P)`, which acts on `P` with a
`VAdd` version of a `DistribMulAction`. -/
instance instMulAction : MulAction G (AffineBasis ι k V) :=
  DFunLike.coe_injective.mulAction _ coe_smul

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