Theorems · Theorem · commutative algebra

LinearEquiv.isScalarTower

∀ {R : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring R] (A : Type u_4) [inst_1 : Semiring A]
  [inst_2 : Module R A] [inst_3 : AddCommMonoid α] [inst_4 : AddCommMonoid β] [inst_5 : Module A β]
  [inst_6 : Module R α] [inst_7 : Module R β] [IsScalarTower R A β] (e : α ≃ₗ[R] β), IsScalarTower R A α

The module instance from AddEquiv.module is compatible with the R-module structures, if the AddEquiv is induced by an R-module isomorphism.

Defined in

Mathlib.Algebra.Module.TransferInstance

Cited by

1 results in Mathlib

Foundations

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

Assumes

SemiringSemiringModuleAddCommMonoidAddCommMonoidModuleModuleModuleIsScalarTower