instMulActionRayVector — Mathlib

English

Any invertible action preserves nonzeroness of ray vectors.

Русский

Любое обратимо значимое действие сохраняет ненулевые лучевые векторы.

LaTeX

$$$ \text{MulAction } G (\text{RayVector } R M) \text{ exists and preserves nonzero elements, i.e. } g \cdot x \neq 0 \text{ if } x \neq 0.$$$

Lean4

/-- Any invertible action preserves the non-zeroness of ray vectors. This is primarily of interest
when `G = Rˣ` -/
instance {R : Type*} : MulAction G (RayVector R M)
    where
  smul r := Subtype.map (r • ·) fun _ => (smul_ne_zero_iff_ne _).2
  mul_smul a b _ := Subtype.ext <| mul_smul a b _
  one_smul _ := Subtype.ext <| one_smul _ _

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