mapLinearEquiv — Mathlib

English

An equivalence between modules implies an equivalence between ray vectors.

Русский

Эквивалентность между модулями порождает эквивалентность между лучами-векторами.

LaTeX

$$$ \text{RayVector.mapLinearEquiv}(e):\text{RayVector}(R,M) \simeq \text{RayVector}(R,N)$ for an equivalence e.$$

Lean4

/-- An equivalence between modules implies an equivalence between ray vectors. -/
def mapLinearEquiv (e : M ≃ₗ[R] N) : RayVector R M ≃ RayVector R N :=
  Equiv.subtypeEquiv e.toEquiv fun _ => e.map_ne_zero_iff.symm

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