Theorems · Theorem · commutative algebra

Equiv.moduleIsTorsionFree

∀ (R : Type u_1) {α : Type u_2} {β : Type u_3} [inst : Semiring R] (e : α ≃ β) [inst_1 : AddCommMonoid β]
  [inst_2 : Module R β] [Module.IsTorsionFree R β],
  let this := e.addCommMonoid;
  have this_1 := Equiv.module R e;
  Module.IsTorsionFree R α

Transfer Module.IsTorsionFree across an Equiv

Defined in

Mathlib.Algebra.Module.TransferInstance

Cited by

0 results in Mathlib

Foundations

Depth 27 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringAddCommMonoidModuleModule.IsTorsionFree