map_apply — Mathlib

English

Applying a linear equivalence to a ray maps the representative nonzero vector to the corresponding ray image.

Русский

При применении линейной эквивалентности к лучу, соответствующий ненулевой вектор переходит к соответствующему лучу-представителю.

LaTeX

$$$ \forall (e:M\simeq_R N)\, (v: M), (hv: v\neq 0), \; \text{Module.Ray.map } e(\text{rayOfNeZero}(R,v,hv)) = \text{rayOfNeZero}(R, e(v), e.map_ne_zero_iff.2 hv). $$$

Lean4

@[simp]
theorem map_apply (e : M ≃ₗ[R] N) (v : M) (hv : v ≠ 0) :
    Module.Ray.map e (rayOfNeZero _ v hv) = rayOfNeZero _ (e v) (e.map_ne_zero_iff.2 hv) :=
  rfl

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