Theorems · Definition · commutative algebra

LinearEquiv.invFun

{R : Type u_14} →
  {S : Type u_15} →
    [inst : Semiring R] →
      [inst_1 : Semiring S] →
        {σ : R →+* S} →
          {σ' : S →+* R} →
            [inst_2 : RingHomInvPair σ σ'] →
              [inst_3 : RingHomInvPair σ' σ] →
                {M : Type u_16} →
                  {M₂ : Type u_17} →
                    [inst_4 : AddCommMonoid M] →
                      [inst_5 : AddCommMonoid M₂] →
                        [inst_6 : Module R M] → [inst_7 : Module S M₂] → (M ≃ₛₗ[σ] M₂) → M₂ → M

The backward map of an equivalence. Do NOT use e.invFun directly. Use the coercion of e.symm instead.

Defined in

Mathlib.Algebra.Module.Equiv.Defs

Cited by

29 results in Mathlib

Foundations

Depth 13 from the axioms · uses no axioms

Assumes

SemiringSemiringRingHomInvPairRingHomInvPairAddCommMonoidAddCommMonoidModuleModule