toSemilinearEquiv — Mathlib

English

The inverse part of a constructed linear equivalence is exactly the provided function inv_fun.

Русский

Обратная часть построенного линейного эквивалентности равна заданной функции inv_fun.

LaTeX

$$coe_symm_mk : (constructed).symm = inv_fun$$

Lean4

/-- Interpret a `RingEquiv` `f` as an `f`-semilinear equiv. -/
@[simps]
def _root_.RingEquiv.toSemilinearEquiv (f : R ≃+* S) :
    haveI := RingHomInvPair.of_ringEquiv f
    haveI := RingHomInvPair.symm (↑f : R →+* S) (f.symm : S →+* R)
    R ≃ₛₗ[(↑f : R →+* S)] S :=
  haveI := RingHomInvPair.of_ringEquiv f
  haveI := RingHomInvPair.symm (↑f : R →+* S) (f.symm : S →+* R)
  { f with
    toFun := f
    map_smul' := f.map_mul }

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