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 _ _