toLinearEquiv — Mathlib

English

The inverse of the linear equivalence corresponding to an additive equivalence equals the linear equivalence of the additive inverse.

Русский

Обратный к линейному эквиваленту, соответствующему аддитивному эквиваленту, равен линейному эквиваленту аддитивного оборота.

LaTeX

$$$ (e.toLinearEquiv h).symm = e.symm $$$

Lean4

/-- `g : R ≃+* S` is `R`-linear when the module structure on `S` is `Module.compHom S g` . -/
@[simps]
def toLinearEquiv {R S : Type*} [Semiring R] [Semiring S] (g : R ≃+* S) :
    haveI := compHom S (↑g : R →+* S)
    R ≃ₗ[R] S :=
  letI := compHom S (↑g : R →+* S)
  { g with
    toFun := (g : R → S)
    invFun := (g.symm : S → R)
    map_smul' := g.map_mul }

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