instEquivLikeLinearEquiv — Mathlib

English

Given a permutation e: ι ≃ ι', there is a linear equivalence between DFinsupp over ι with M_i and DFinsupp over ι' with M_{e^{-1}(i)}.

Русский

При заданном биективном отображении e: ι ≃ ι' существует линейное эквалентное отображение между DFinsupp над ι с M_i и DFinsupp над ι' с M_{e^{-1}(i)}.

LaTeX

$$$\\text{domLCongr}(e) : (Π_0 i, M_i) \\simeq_ℓ (Π_0 i, M_{e.symm i})$$$

Lean4

instance {R : Type*} {S : Type*} [Semiring R] [Semiring S] (σ : R →+* S) {σ' : S →+* R} [RingHomInvPair σ σ']
    [RingHomInvPair σ' σ] (M : Type*) (M₂ : Type*) [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] :
    EquivLike (LinearEquiv σ M M₂) M M₂ :=
  inferInstance

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