symm_bijective — Mathlib

English

The operation that sends a semilinear equivalence e to its inverse e.symm is a bijection between the class of σ-semilinear equivalences M ≃σ M₂ and the class of σ'-semilinear equivalences M₂ ≃σ' M.

Русский

Операция перехода элементы в их обратные эквиваленты образует биекцию между множествами σ-полу-линейных эквивалентностей M ≃σ M₂ и M₂ ≃σ' M.

LaTeX

$$Bijective(symm : (M ≃σ M₂) → M₂ ≃σ' M)$$

Lean4

theorem symm_bijective [Module R M] [Module S M₂] [RingHomInvPair σ' σ] [RingHomInvPair σ σ'] :
    Function.Bijective (symm : (M ≃ₛₗ[σ] M₂) → M₂ ≃ₛₗ[σ'] M) :=
  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

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