Theorems · Definition · geometry

AffineSubspace.pointwiseSMul

{M : Type u_1} →
  {k : Type u_2} →
    {V : Type u_3} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V] →
          [inst_2 : Module k V] → [inst_3 : DistribSMul M V] → [SMulCommClass M k V] → SMul M (AffineSubspace k V)

The multiplicative action on an affine subspace corresponding to applying the action to every element. This is available as an instance in the Pointwise locale. TODO: generalize to include SMul (P ≃ᵃ[k] P) (AffineSubspace k P), which acts on P with a VAdd version of a DistribMulAction.

Defined in

Mathlib.LinearAlgebra.AffineSpace.Pointwise

Cited by

9 results in Mathlib

Foundations

Depth 31 from the axioms · uses propext, Quot.sound

Assumes

RingAddCommGroupModuleDistribSMulSMulCommClass