linearEquiv_toAddEquiv — Mathlib

English

The additive structure induced by mapRange.linearEquiv f coincides with the additive equivalence obtained from f.toAddEquiv.

Русский

Аддитивная структура, индуцированная mapRange.linearEquiv f, совпадает с аддитивным эквивариантом, полученным из f.toAddEquiv.

LaTeX

$$$$ (mapRange.linearEquiv f).toAddEquiv = (mapRange.addEquiv f.toAddEquiv). $$$$

Lean4

@[simp]
theorem linearEquiv_toAddEquiv (f : M ≃ₛₗ[σ₁₂] N) :
    (mapRange.linearEquiv f).toAddEquiv = (mapRange.addEquiv f.toAddEquiv : (α →₀ M) ≃+ _) :=
  AddEquiv.ext fun _ => rfl

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