Documentation Verification Report

TransferInstance

📁 Source: Mathlib/Algebra/Module/TransferInstance.lean

Statistics

Metric	Count
Definitions `linearEquiv`, `linearEquiv`	2
Theorems `linearEquiv_apply`, `linearEquiv_symm_apply`, `moduleIsTorsionFree`, `noZeroSMulDivisors`, `isScalarTower`	5
Total	7

AddEquiv

Definitions

Name	Category	Theorems
`linearEquiv` 📖	CompOp	2 math math: `linearEquiv_symm_apply`, `linearEquiv_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`linearEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `linearEquiv` `Equiv.toFun` `toEquiv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`RingHomInvPair.ids`
`linearEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `linearEquiv` `Equiv.invFun` `toEquiv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`RingHomInvPair.ids`

Equiv

Definitions

Name	Category	Theorems
`linearEquiv` 📖	CompOp	3 math math: `tensorProductAssoc_def`, `toLinearEquiv_continuousLinearEquiv`, `tensorProductComm_def`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`moduleIsTorsionFree` 📖	mathematical	—	`addCommMonoid` `module`	—	`Function.Injective.moduleIsTorsionFree` `RingHomInvPair.ids` `LinearEquiv.injective` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass`
`noZeroSMulDivisors` 📖	mathematical	—	`zero` `smul`	—	`apply_symm_apply` `NoZeroSMulDivisors.eq_zero_or_eq_zero_of_smul_eq_zero`

LinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isScalarTower` 📖	mathematical	—	`IsScalarTower` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddCommMonoid.toAddMonoid` `AddEquiv.module` `toAddEquiv` `RingHom.id` `RingHomInvPair.ids`	—	`RingHomInvPair.ids` `left_inv` `right_inv` `smul_assoc` `map_smul`

---

← Back to Index