Documentation Verification Report

Bimodule

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

Statistics

Metric	Count
Definitions `baseChange`, `mk`, `toSubbimoduleInt`, `toSubbimoduleNat`, `toSubmodule`, `toSubmodule'`	6
Theorems `coe_baseChange`, `coe_mk`, `coe_toSubbimoduleInt`, `coe_toSubbimoduleNat`, `coe_toSubmodule`, `coe_toSubmodule'`, `smul_mem`, `smul_mem'`	8
Total	14

Subbimodule

Definitions

Name	Category	Theorems
`baseChange` 📖	CompOp	1 math math: `coe_baseChange`
`mk` 📖	CompOp	—
`toSubbimoduleInt` 📖	CompOp	1 math math: `coe_toSubbimoduleInt`
`toSubbimoduleNat` 📖	CompOp	1 math math: `coe_toSubbimoduleNat`
`toSubmodule` 📖	CompOp	1 math math: `coe_toSubmodule`
`toSubmodule'` 📖	CompOp	1 math math: `coe_toSubmodule'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_baseChange` 📖	mathematical	—	`SetLike.coe` `Submodule` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Algebra.TensorProduct.instSemiring` `TensorProduct.Algebra.module` `Submodule.setLike` `baseChange`	—	—
`coe_mk` 📖	mathematical	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SetLike.instMembership` `AddSubmonoid.instSetLike` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	`SetLike.coe` `Submodule` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Algebra.TensorProduct.instSemiring` `TensorProduct.Algebra.module` `Submodule.setLike` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddSubmonoid.instSetLike`	—	—
`coe_toSubbimoduleInt` 📖	mathematical	—	`SetLike.coe` `Submodule` `TensorProduct` `Int.instCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddCommGroup.toIntModule` `Ring.toAddCommGroup` `Algebra.TensorProduct.instSemiring` `Ring.toSemiring` `Ring.toIntAlgebra` `AddCommGroup.toAddCommMonoid` `TensorProduct.Algebra.module` `AddCommGroup.intIsScalarTower` `Submodule.setLike` `toSubbimoduleInt` `Nat.instCommSemiring` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Semiring.toNatAlgebra` `AddCommMonoid.toNatModule`	—	`AddCommMonoid.nat_isScalarTower` `AddCommGroup.intIsScalarTower`
`coe_toSubbimoduleNat` 📖	mathematical	—	`SetLike.coe` `Submodule` `TensorProduct` `Nat.instCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddCommMonoid.toNatModule` `Algebra.TensorProduct.instSemiring` `Ring.toSemiring` `Semiring.toNatAlgebra` `AddCommGroup.toAddCommMonoid` `TensorProduct.Algebra.module` `AddCommMonoid.nat_isScalarTower` `Submodule.setLike` `toSubbimoduleNat` `Int.instCommSemiring` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Ring.toIntAlgebra` `AddCommGroup.toIntModule` `AddCommGroup.intIsScalarTower`	—	`AddCommGroup.intIsScalarTower` `AddCommMonoid.nat_isScalarTower`
`coe_toSubmodule` 📖	mathematical	—	`SetLike.coe` `Submodule` `Submodule.setLike` `toSubmodule` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Algebra.TensorProduct.instSemiring` `TensorProduct.Algebra.module`	—	—
`coe_toSubmodule'` 📖	mathematical	—	`SetLike.coe` `Submodule` `Submodule.setLike` `toSubmodule'` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Algebra.TensorProduct.instSemiring` `TensorProduct.Algebra.module`	—	—
`smul_mem` 📖	mathematical	`Submodule` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Algebra.TensorProduct.instSemiring` `TensorProduct.Algebra.module` `SetLike.instMembership` `Submodule.setLike`	`Submodule` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Algebra.TensorProduct.instSemiring` `TensorProduct.Algebra.module` `SetLike.instMembership` `Submodule.setLike` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`one_smul` `Submodule.smul_mem`
`smul_mem'` 📖	mathematical	`Submodule` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Algebra.TensorProduct.instSemiring` `TensorProduct.Algebra.module` `SetLike.instMembership` `Submodule.setLike`	`Submodule` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Algebra.TensorProduct.instSemiring` `TensorProduct.Algebra.module` `SetLike.instMembership` `Submodule.setLike` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`one_smul` `Submodule.smul_mem`

---

← Back to Index