smulOfNeZero — Mathlib

English

Multiplying by a nonzero scalar a in a field K is a linear isomorphism of the K-vector space M; its inverse is multiplication by a⁻¹.

Русский

Умножение на ненулевой скаляр a в поле K является линейным изоморфизмом пространства M над K; обратное отображение — умножение на a⁻¹.

LaTeX

$$$ a \neq 0 \Rightarrow (M \simeq_{\text{linear}} M), \; v \mapsto a v \text{ is a linear isomorphism with inverse } v \mapsto a^{-1} v $$$

Lean4

/-- Multiplying by a nonzero element `a` of the field `K` is a linear equivalence. -/
@[simps!]
def smulOfNeZero (a : K) (ha : a ≠ 0) : M ≃ₗ[K] M :=
  smulOfUnit <| Units.mk0 a ha

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