Transfer algebraic structures across Equivs or AddEquivs

This continues the pattern set in Mathlib/Algebra/Group/TransferInstance.lean.

theorem Equiv.noZeroSMulDivisors {α : Type u_2} {β : Type u_3} (R : Type u_4) [Zero R] [Zero α] [Zero β] [SMul R β] [NoZeroSMulDivisors R β] (e : α ≃ β) (map_zero : e 0 = 0) : NoZeroSMulDivisors R α

Transfer NoZeroSMulDivisors across an Equiv

@[reducible, inline]

abbrev AddEquiv.module (R : Type u_1) {α : Type u_2} {β : Type u_3} [Semiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R β] (e : α ≃+ β) : Module R α

Transfer Module across an Equiv

Equations

• AddEquiv.module R e = { toDistribMulAction := AddEquiv.distribMulAction R e, add_smul := ⋯, zero_smul := ⋯ }

def AddEquiv.linearEquiv (R : Type u_1) {α : Type u_2} {β : Type u_3} [Semiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R β] (e : α ≃+ β) : α ≃ₗ[R] β

When α is equipped with the A-module structure transferred via e : α ≃+ β, this isomorphism is A-linear.

Equations

• AddEquiv.linearEquiv R e = { toFun := e.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem AddEquiv.linearEquiv_apply {R : Type u_1} {α : Type u_2} {β : Type u_3} [Semiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R β] (e : α ≃+ β) (a : α) : (linearEquiv R e) a = e a

@[simp]

theorem AddEquiv.linearEquiv_symm_apply {R : Type u_1} {α : Type u_2} {β : Type u_3} [Semiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R β] (e : α ≃+ β) (b : β) : (linearEquiv R e).symm b = e.symm b

theorem AddEquiv.moduleIsTorsionFree (R : Type u_1) {α : Type u_2} {β : Type u_3} [Semiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R β] (e : α ≃+ β) [Module.IsTorsionFree R β] : Module.IsTorsionFree R α

Transfer Module.IsTorsionFree across an Equiv

@[deprecated AddEquiv.module (since := "2026-08-10")]

def Equiv.module (R : Type u_1) {α : Type u_2} {β : Type u_3} [Semiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R β] (e : α ≃+ β) : Module R α

Alias of AddEquiv.module.

---

Transfer Module across an Equiv

Equations

• Equiv.module = AddEquiv.module

@[deprecated AddEquiv.linearEquiv (since := "2026-08-10")]

def Equiv.linearEquiv (R : Type u_1) {α : Type u_2} {β : Type u_3} [Semiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R β] (e : α ≃+ β) : α ≃ₗ[R] β

Alias of AddEquiv.linearEquiv.

---

When α is equipped with the A-module structure transferred via e : α ≃+ β, this isomorphism is A-linear.

Equations

• Equiv.linearEquiv = AddEquiv.linearEquiv

@[deprecated AddEquiv.linearEquiv_apply (since := "2026-08-10")]

theorem Equiv.linearEquiv_apply {R : Type u_1} {α : Type u_2} {β : Type u_3} [Semiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R β] (e : α ≃+ β) (a : α) : (AddEquiv.linearEquiv R e) a = e a

Alias of AddEquiv.linearEquiv_apply.

@[deprecated AddEquiv.linearEquiv_symm_apply (since := "2026-08-10")]

theorem Equiv.linearEquiv_symm_apply {R : Type u_1} {α : Type u_2} {β : Type u_3} [Semiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R β] (e : α ≃+ β) (b : β) : (AddEquiv.linearEquiv R e).symm b = e.symm b

Alias of AddEquiv.linearEquiv_symm_apply.

@[deprecated AddEquiv.moduleIsTorsionFree (since := "2026-08-10")]

theorem Equiv.moduleIsTorsionFree (R : Type u_1) {α : Type u_2} {β : Type u_3} [Semiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R β] (e : α ≃+ β) [Module.IsTorsionFree R β] : Module.IsTorsionFree R α

Alias of AddEquiv.moduleIsTorsionFree.

---

Transfer Module.IsTorsionFree across an Equiv

theorem LinearEquiv.isScalarTower {R : Type u_1} {α : Type u_2} {β : Type u_3} [Semiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R β] [Module R α] (A : Type u_4) [Semiring A] [Module R A] [Module A β] [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.