toLinearEquiv — Mathlib

English

An additive equivalence that preserves scalar multiplication is a linear equivalence.

Русский

Аддитивное эквивалентное отображение, сохраняющее умножение на скаляры, является линейным эквивалентом.

LaTeX

$$$ toLinearEquiv (h) : M \simeq_R M_2 $$$

Lean4

/-- An additive equivalence whose underlying function preserves `smul` is a linear equivalence. -/
def toLinearEquiv (h : ∀ (c : R) (x), e (c • x) = c • e x) : M ≃ₗ[R] M₂ :=
  { e with map_smul' := h }

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