Documentation Verification Report

RestrictScalars

📁 Source: Mathlib/Algebra/Algebra/RestrictScalars.lean

Statistics

Metric	Count
Definitions `restrictScalars`, `restrictScalars`, `addEquiv`, `algebra`, `lsmul`, `moduleOrig`, `opModule`, `ringEquiv`, `instAddCommGroupRestrictScalars`, `instAddCommMonoidRestrictScalars`, `instCommRingRestrictScalars`, `instCommSemiringRestrictScalars`, `instInhabitedRestrictScalars`, `instRingRestrictScalars`, `instSemiringRestrictScalars`	15
Theorems `restrictScalars`, `addEquiv_map_smul`, `addEquiv_symm_map_algebraMap_smul`, `addEquiv_symm_map_smul_smul`, `isCentralScalar`, `isScalarTower`, `lsmul_apply_apply`, `ringEquiv_algebraMap`, `ringEquiv_map_smul`, `smul_def`	10
Total	25

Algebra

Definitions

Name	Category	Theorems
`restrictScalars` 📖	CompOp	—

IsScalarTower

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`restrictScalars` 📖	mathematical	—	`IsScalarTower` `Algebra.toSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `CommSemiring.toSemiring` `Module.restrictScalars`	—	`of_compHom`

Module

Definitions

Name	Category	Theorems
`restrictScalars` 📖	CompOp	1 math math: `IsScalarTower.restrictScalars`

RestrictScalars

Definitions

Name	Category	Theorems
`addEquiv` 📖	CompOp	8 math math: `Representation.smul_ofModule_asModule`, `Representation.ofModule_asModule_act`, `lsmul_apply_apply`, `addEquiv_symm_map_smul_smul`, `Representation.ofModule_asAlgebraHom_apply_apply`, `addEquiv_symm_map_algebraMap_smul`, `smul_def`, `addEquiv_map_smul`
`algebra` 📖	CompOp	1 math math: `ringEquiv_algebraMap`
`lsmul` 📖	CompOp	1 math math: `lsmul_apply_apply`
`moduleOrig` 📖	CompOp	1 math math: `isScalarTower`
`opModule` 📖	CompOp	1 math math: `isCentralScalar`
`ringEquiv` 📖	CompOp	2 math math: `ringEquiv_algebraMap`, `ringEquiv_map_smul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addEquiv_map_smul` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `RestrictScalars` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoidRestrictScalars` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `addEquiv` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Module.toDistribMulAction` `module` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap`	—	—
`addEquiv_symm_map_algebraMap_smul` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `RestrictScalars` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoidRestrictScalars` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `addEquiv` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap` `module`	—	—
`addEquiv_symm_map_smul_smul` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `RestrictScalars` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoidRestrictScalars` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `addEquiv` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.toSMul` `CommSemiring.toSemiring` `module`	—	`Algebra.smul_def` `SemigroupAction.mul_smul`
`isCentralScalar` 📖	mathematical	—	`IsCentralScalar` `RestrictScalars` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidRestrictScalars` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Module.toDistribMulAction` `module` `MulOpposite` `MulOpposite.instMonoid` `MulOpposite.instSemiring` `opModule`	—	`IsCentralScalar.op_smul_eq_smul`
`isScalarTower` 📖	mathematical	—	`IsScalarTower` `RestrictScalars` `Algebra.toSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidRestrictScalars` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `moduleOrig` `CommSemiring.toSemiring` `module`	—	`IsScalarTower.restrictScalars`
`lsmul_apply_apply` 📖	mathematical	—	`DFunLike.coe` `Module.End` `RestrictScalars` `CommSemiring.toSemiring` `instAddCommMonoidRestrictScalars` `module` `LinearMap.instFunLike` `RingHom.id` `Semiring.toNonAssocSemiring` `AlgHom` `Module.End.instSemiring` `Module.End.instAlgebra` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Algebra.toSMul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AlgHom.funLike` `lsmul` `AddEquiv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `addEquiv` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul`	—	`smulCommClass_self` `IsScalarTower.left`
`ringEquiv_algebraMap` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `RestrictScalars` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringRestrictScalars` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `ringEquiv` `RingHom` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap` `algebra`	—	—
`ringEquiv_map_smul` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `RestrictScalars` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringRestrictScalars` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `ringEquiv` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Module.toDistribMulAction` `instAddCommMonoidRestrictScalars` `NonUnitalNonAssocSemiring.toAddCommMonoid` `module` `Algebra.toModule` `Algebra.toSMul` `RingHom` `RingHom.instFunLike` `algebraMap`	—	—
`smul_def` 📖	mathematical	—	`RestrictScalars` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidRestrictScalars` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Module.toDistribMulAction` `module` `DFunLike.coe` `AddEquiv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `addEquiv` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap`	—	—

(root)

Definitions

Name	Category	Theorems
`instAddCommGroupRestrictScalars` 📖	CompOp	3 math math: `Representation.isSimpleModule_iff_irreducible_ofModule`, `Representation.is_simple_module_iff_irreducible_ofModule`, `Representation.isSemisimpleModule_iff_isSemisimpleRepresentation_ofModule`
`instAddCommMonoidRestrictScalars` 📖	CompOp	15 math math: `Representation.smul_ofModule_asModule`, `Subrepresentation.mem_asSubmodule'_iff`, `Subrepresentation.submoduleSubrepresentationOrderIso_apply`, `Representation.ofModule_asModule_act`, `RestrictScalars.ringEquiv_map_smul`, `RestrictScalars.lsmul_apply_apply`, `RestrictScalars.addEquiv_symm_map_smul_smul`, `RestrictScalars.isScalarTower`, `Representation.ofModule_asAlgebraHom_apply_apply`, `Subrepresentation.mem_ofSubmodule_iff`, `RestrictScalars.isCentralScalar`, `RestrictScalars.addEquiv_symm_map_algebraMap_smul`, `RestrictScalars.smul_def`, `Subrepresentation.submoduleSubrepresentationOrderIso_symm_apply`, `RestrictScalars.addEquiv_map_smul`
`instCommRingRestrictScalars` 📖	CompOp	—
`instCommSemiringRestrictScalars` 📖	CompOp	—
`instInhabitedRestrictScalars` 📖	CompOp	—
`instRingRestrictScalars` 📖	CompOp	—
`instSemiringRestrictScalars` 📖	CompOp	2 math math: `RestrictScalars.ringEquiv_algebraMap`, `RestrictScalars.ringEquiv_map_smul`

---

← Back to Index