pointwiseAddAction — Mathlib

English

The additive action of V on AffineSubspace k P forms an AddAction, i.e., shifting by a vector defines a compatible action on subspaces.

Русский

Аддитивное действие V на AffineSubspace k P образует AddAction: перенос на вектор задаёт совместное действие на подплощадях.

LaTeX

$$$\text{pointwiseAddAction}:\ V \curvearrowright (\mathrm{AffineSubspace}\ k\ P).$$$

Lean4

/-- The additive action on an affine subspace corresponding to applying the action to every element.

This is available as an instance in the `Pointwise` locale. -/
protected def pointwiseAddAction : AddAction V (AffineSubspace k P) :=
  SetLike.coe_injective.addAction _ coe_pointwise_vadd

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