symm_apply — Mathlib

English

The symmetry map e.symm acts as the inverse on M₂.

Русский

Симметрия e.symm действует как обратное отображение на M₂.

LaTeX

$$LinearEquiv.Simps.symm : M ≃ M₂ → M₂ → M$$

Lean4

/-- See Note [custom simps projection] -/
def symm_apply {R S : Type*} [Semiring R] [Semiring S] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ']
    [RingHomInvPair σ' σ] {M M₂ : Type*} [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂]
    (e : M ≃ₛₗ[σ] M₂) : M₂ → M :=
  e.symm

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