Theorems · Definition · commutative algebra

Equiv.module

(R : Type u_1) →
  {α : Type u_2} →
    {β : Type u_3} → [inst : Semiring R] → (e : α ≃ β) → [inst_1 : AddCommMonoid β] → [Module R β] → Module R α

Transfer Module across an Equiv

Defined in

Mathlib.Algebra.Module.TransferInstance

Cited by

8 results in Mathlib

Foundations

Depth 22 from the axioms · uses propext, Quot.sound

Assumes

SemiringAddCommMonoidModule