smul_rayOfNeZero — Mathlib

English

If g is an element of G and v ≠ 0 in M, then acting by g on the rayOfNeZero associated to v yields the rayOfNeZero associated to g·v. The nonzeroness is preserved by smul.

Русский

Если g из G и v ≠ 0 в M, то действие на луч из v аналогично лучу из g·v; ненулевость сохраняется при умножении.

LaTeX

$$$g\cdot \mathrm{rayOfNeZero}(R,v,hv)=\mathrm{rayOfNeZero}(R,g\cdot v,(\smul\_ne\_zero\_iff\_ne\ _).2 hv).$$$

Lean4

@[simp]
theorem smul_rayOfNeZero (g : G) (v : M) (hv) :
    g • rayOfNeZero R v hv = rayOfNeZero R (g • v) ((smul_ne_zero_iff_ne _).2 hv) :=
  rfl

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