TransferInstance

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

Statistics

Metric	Count
Definitions linearEquiv	1
Theorems moduleIsTorsionFree, noZeroSMulDivisors, isScalarTower	3
Total	4

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