Documentation Verification Report

Subalgebra

📁 Source: Mathlib/LinearAlgebra/TensorProduct/Subalgebra.lean

Statistics

Metric	Count
Definitions `algEquivIncludeRange`, `linearEquivIncludeRange`, `lTensorBot`, `mulMap`, `mulMap'`, `rTensorBot`	6
Theorems `algEquivIncludeRange_symm_tmul`, `algEquivIncludeRange_symm_toAlgHom`, `algEquivIncludeRange_tmul`, `algEquivIncludeRange_toAlgHom`, `linearEquivIncludeRange_symm_tmul`, `linearEquivIncludeRange_symm_toLinearMap`, `linearEquivIncludeRange_tmul`, `linearEquivIncludeRange_toLinearMap`, `comm_trans_lTensorBot`, `comm_trans_rTensorBot`, `lTensorBot_one_tmul`, `lTensorBot_symm_apply`, `lTensorBot_tmul`, `mulMap'_surjective`, `mulMap_bot_left_eq`, `mulMap_bot_right_eq`, `mulMap_comm`, `mulMap_map_comp_eq`, `mulMap_range`, `mulMap_tmul`, `mulMap_toLinearMap`, `rTensorBot_symm_apply`, `rTensorBot_tmul`, `rTensorBot_tmul_one`, `val_mulMap'_tmul`	25
Total	31

Algebra.TensorProduct

Definitions

Name	Category	Theorems
`algEquivIncludeRange` 📖	CompOp	4 math math: `algEquivIncludeRange_symm_tmul`, `algEquivIncludeRange_tmul`, `algEquivIncludeRange_toAlgHom`, `algEquivIncludeRange_symm_toAlgHom`
`linearEquivIncludeRange` 📖	CompOp	4 math math: `linearEquivIncludeRange_toLinearMap`, `linearEquivIncludeRange_symm_tmul`, `linearEquivIncludeRange_symm_toLinearMap`, `linearEquivIncludeRange_tmul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algEquivIncludeRange_symm_tmul` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Subalgebra` `instSemiring` `leftAlgebra` `SetLike.instMembership` `Subalgebra.instSetLike` `AlgHom.range` `includeLeft` `instAlgebra` `includeRight` `Subalgebra.toSemiring` `Subalgebra.instModuleSubtypeMem` `Subalgebra.algebra` `AlgEquiv.instFunLike` `AlgEquiv.symm` `algEquivIncludeRange` `TensorProduct.tmul` `instMul` `Algebra.to_smulCommClass` `IsScalarTower.right`	—	—
`algEquivIncludeRange_symm_toAlgHom` 📖	mathematical	—	`AlgEquiv.toAlgHom` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Algebra.toModule` `Subalgebra` `instSemiring` `leftAlgebra` `SetLike.instMembership` `Subalgebra.instSetLike` `AlgHom.range` `includeLeft` `instAlgebra` `includeRight` `Subalgebra.toSemiring` `Subalgebra.instModuleSubtypeMem` `Subalgebra.algebra` `AlgEquiv.symm` `algEquivIncludeRange` `Subalgebra.mulMap` `instCommSemiring`	—	—
`algEquivIncludeRange_tmul` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Subalgebra` `instSemiring` `leftAlgebra` `SetLike.instMembership` `Subalgebra.instSetLike` `AlgHom.range` `includeLeft` `instAlgebra` `includeRight` `Subalgebra.toSemiring` `Subalgebra.instModuleSubtypeMem` `Subalgebra.algebra` `AlgEquiv.instFunLike` `algEquivIncludeRange` `TensorProduct.tmul` `AlgHom` `AlgHom.funLike` `AlgHom.rangeRestrict`	—	—
`algEquivIncludeRange_toAlgHom` 📖	mathematical	—	`AlgEquiv.toAlgHom` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Subalgebra` `instSemiring` `leftAlgebra` `SetLike.instMembership` `Subalgebra.instSetLike` `AlgHom.range` `includeLeft` `instAlgebra` `includeRight` `Subalgebra.toSemiring` `Subalgebra.instModuleSubtypeMem` `Subalgebra.algebra` `algEquivIncludeRange` `map` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Subalgebra.instIsScalarTowerSubtypeMem` `Algebra.toSMul` `AlgHom.rangeRestrict`	—	—
`linearEquivIncludeRange_symm_tmul` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `Subalgebra` `instSemiring` `leftAlgebra` `SetLike.instMembership` `Subalgebra.instSetLike` `AlgHom.range` `includeLeft` `instAlgebra` `includeRight` `Subalgebra.toSemiring` `Subalgebra.instModuleSubtypeMem` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `linearEquivIncludeRange` `TensorProduct.tmul` `instMul` `Algebra.to_smulCommClass` `IsScalarTower.right`	—	`RingHomInvPair.ids`
`linearEquivIncludeRange_symm_toLinearMap` 📖	mathematical	—	`LinearEquiv.toLinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `Subalgebra` `instSemiring` `leftAlgebra` `SetLike.instMembership` `Subalgebra.instSetLike` `AlgHom.range` `includeLeft` `instAlgebra` `includeRight` `Subalgebra.toSemiring` `Subalgebra.instModuleSubtypeMem` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearEquiv.symm` `linearEquivIncludeRange` `Submodule.mulMap` `LinearMap.range` `RingHomSurjective.ids` `AlgHom.toLinearMap`	—	`RingHomInvPair.ids`
`linearEquivIncludeRange_tmul` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `Subalgebra` `instSemiring` `leftAlgebra` `SetLike.instMembership` `Subalgebra.instSetLike` `AlgHom.range` `includeLeft` `instAlgebra` `includeRight` `Subalgebra.toSemiring` `Subalgebra.instModuleSubtypeMem` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `linearEquivIncludeRange` `TensorProduct.tmul` `AlgHom` `Subalgebra.algebra` `AlgHom.funLike` `AlgHom.rangeRestrict`	—	`RingHomInvPair.ids`
`linearEquivIncludeRange_toLinearMap` 📖	mathematical	—	`LinearEquiv.toLinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `Subalgebra` `instSemiring` `leftAlgebra` `SetLike.instMembership` `Subalgebra.instSetLike` `AlgHom.range` `includeLeft` `instAlgebra` `includeRight` `Subalgebra.toSemiring` `Subalgebra.instModuleSubtypeMem` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `linearEquivIncludeRange` `TensorProduct.map` `Submodule` `Submodule.setLike` `LinearMap.range` `RingHomSurjective.ids` `AlgHom.toLinearMap` `Submodule.addCommMonoid` `Submodule.module` `LinearMap.rangeRestrict`	—	`RingHomInvPair.ids`

Subalgebra

Definitions

Name	Category	Theorems
`lTensorBot` 📖	CompOp	6 math math: `comm_trans_rTensorBot`, `lTensorBot_one_tmul`, `mulMap_bot_left_eq`, `lTensorBot_symm_apply`, `lTensorBot_tmul`, `comm_trans_lTensorBot`
`mulMap` 📖	CompOp	9 math math: `mulMap_comm`, `mulMap_toLinearMap`, `mulMap_map_comp_eq`, `mulMap_bot_left_eq`, `mulMap_bot_right_eq`, `linearDisjoint_iff_injective`, `mulMap_range`, `Algebra.TensorProduct.algEquivIncludeRange_symm_toAlgHom`, `mulMap_tmul`
`mulMap'` 📖	CompOp	2 math math: `mulMap'_surjective`, `val_mulMap'_tmul`
`rTensorBot` 📖	CompOp	6 math math: `comm_trans_rTensorBot`, `rTensorBot_tmul_one`, `mulMap_bot_right_eq`, `rTensorBot_symm_apply`, `comm_trans_lTensorBot`, `rTensorBot_tmul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comm_trans_lTensorBot` 📖	mathematical	—	`AlgEquiv.trans` `TensorProduct` `Subalgebra` `SetLike.instMembership` `instSetLike` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `toSemiring` `Algebra.toModule` `algebra` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.instAlgebra` `Algebra.TensorProduct.comm` `lTensorBot` `rTensorBot`	—	`AlgEquiv.toLinearEquiv_injective` `Submodule.comm_trans_lTensorOne`
`comm_trans_rTensorBot` 📖	mathematical	—	`AlgEquiv.trans` `TensorProduct` `Subalgebra` `SetLike.instMembership` `instSetLike` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `toSemiring` `Algebra.toModule` `algebra` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.instAlgebra` `Algebra.TensorProduct.comm` `rTensorBot` `lTensorBot`	—	`AlgEquiv.toLinearEquiv_injective` `Submodule.comm_trans_rTensorOne`
`lTensorBot_one_tmul` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `TensorProduct` `Subalgebra` `SetLike.instMembership` `instSetLike` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `toSemiring` `instModuleSubtypeMem` `Algebra.TensorProduct.instSemiring` `algebra` `Algebra.TensorProduct.instAlgebra` `AlgEquiv.instFunLike` `lTensorBot` `TensorProduct.tmul` `OneMemClass.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddSubmonoidWithOneClass.toOneMemClass` `SubsemiringClass.addSubmonoidWithOneClass` `instSubsemiringClass`	—	`Submodule.lTensorOne_one_tmul`
`lTensorBot_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Subalgebra` `SetLike.instMembership` `instSetLike` `TensorProduct` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `toSemiring` `instModuleSubtypeMem` `Algebra.TensorProduct.instSemiring` `algebra` `Algebra.TensorProduct.instAlgebra` `AlgEquiv.instFunLike` `AlgEquiv.symm` `lTensorBot` `TensorProduct.tmul` `OneMemClass.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddSubmonoidWithOneClass.toOneMemClass` `SubsemiringClass.addSubmonoidWithOneClass` `instSubsemiringClass`	—	—
`lTensorBot_tmul` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `TensorProduct` `Subalgebra` `SetLike.instMembership` `instSetLike` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `toSemiring` `instModuleSubtypeMem` `Algebra.TensorProduct.instSemiring` `algebra` `Algebra.TensorProduct.instAlgebra` `AlgEquiv.instFunLike` `lTensorBot` `TensorProduct.tmul` `RingHom` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap` `Algebra.toSMul`	—	`Submodule.lTensorOne_tmul`
`mulMap'_surjective` 📖	mathematical	—	`TensorProduct` `Subalgebra` `CommSemiring.toSemiring` `SetLike.instMembership` `instSetLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `toSemiring` `instModuleSubtypeMem` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Algebra.instCompleteLatticeSubalgebra` `DFunLike.coe` `AlgHom` `Algebra.TensorProduct.instSemiring` `algebra` `Algebra.TensorProduct.instAlgebra` `AlgHom.funLike` `mulMap'`	—	`mulMap_range` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass`
`mulMap_bot_left_eq` 📖	mathematical	—	`mulMap` `Bot.bot` `Subalgebra` `CommSemiring.toSemiring` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `AlgHom.comp` `TensorProduct` `SetLike.instMembership` `instSetLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `toSemiring` `instModuleSubtypeMem` `Algebra.TensorProduct.instSemiring` `algebra` `Algebra.TensorProduct.instAlgebra` `val` `AlgEquiv.toAlgHom` `lTensorBot`	—	`AlgHom.toLinearMap_injective` `Submodule.mulMap_one_left_eq`
`mulMap_bot_right_eq` 📖	mathematical	—	`mulMap` `Bot.bot` `Subalgebra` `CommSemiring.toSemiring` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `AlgHom.comp` `TensorProduct` `SetLike.instMembership` `instSetLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `toSemiring` `instModuleSubtypeMem` `Algebra.TensorProduct.instSemiring` `algebra` `Algebra.TensorProduct.instAlgebra` `val` `AlgEquiv.toAlgHom` `rTensorBot`	—	`AlgHom.toLinearMap_injective` `Submodule.mulMap_one_right_eq`
`mulMap_comm` 📖	mathematical	—	`mulMap` `AlgHom.comp` `TensorProduct` `Subalgebra` `CommSemiring.toSemiring` `SetLike.instMembership` `instSetLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `toSemiring` `instModuleSubtypeMem` `Algebra.TensorProduct.instSemiring` `algebra` `Algebra.TensorProduct.instAlgebra` `AlgHomClass.toAlgHom` `AlgEquiv` `Algebra.toModule` `AlgEquiv.instFunLike` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instEquivLike` `AlgEquiv.instAlgEquivClass` `Algebra.TensorProduct.comm`	—	`Algebra.TensorProduct.ext` `instIsScalarTowerSubtypeMem` `IsScalarTower.left` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `AlgHom.ext` `IsScalarTower.to_smulCommClass` `mul_one` `one_mul` `TensorProduct.isScalarTower_left`
`mulMap_map_comp_eq` 📖	mathematical	—	`AlgHom.comp` `TensorProduct` `Subalgebra` `CommSemiring.toSemiring` `SetLike.instMembership` `instSetLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `toSemiring` `Algebra.toModule` `algebra` `map` `instModuleSubtypeMem` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.leftAlgebra` `IsScalarTower.to_smulCommClass` `Algebra.id` `instIsScalarTowerSubtypeMem` `Algebra.toSMul` `Algebra.TensorProduct.instAlgebra` `mulMap` `Algebra.TensorProduct.map` `AlgHom.subalgebraMap`	—	`Algebra.TensorProduct.ext` `instIsScalarTowerSubtypeMem` `IsScalarTower.left` `IsScalarTower.to_smulCommClass` `AlgHom.ext` `AddSubmonoidWithOneClass.toOneMemClass` `SubsemiringClass.addSubmonoidWithOneClass` `instSubsemiringClass` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `mul_one` `TensorProduct.isScalarTower_left` `one_mul`
`mulMap_range` 📖	mathematical	—	`AlgHom.range` `TensorProduct` `Subalgebra` `CommSemiring.toSemiring` `SetLike.instMembership` `instSetLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `toSemiring` `instModuleSubtypeMem` `Algebra.TensorProduct.instSemiring` `algebra` `Algebra.TensorProduct.instAlgebra` `mulMap` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Algebra.instCompleteLatticeSubalgebra`	—	`Algebra.TensorProduct.productMap_range` `range_val`
`mulMap_tmul` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `TensorProduct` `Subalgebra` `CommSemiring.toSemiring` `SetLike.instMembership` `instSetLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `toSemiring` `instModuleSubtypeMem` `Algebra.TensorProduct.instSemiring` `algebra` `Algebra.TensorProduct.instAlgebra` `AlgHom.funLike` `mulMap` `TensorProduct.tmul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	—
`mulMap_toLinearMap` 📖	mathematical	—	`AlgHom.toLinearMap` `TensorProduct` `Subalgebra` `CommSemiring.toSemiring` `SetLike.instMembership` `instSetLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `toSemiring` `instModuleSubtypeMem` `Algebra.TensorProduct.instSemiring` `algebra` `Algebra.TensorProduct.instAlgebra` `mulMap` `Submodule.mulMap` `DFunLike.coe` `OrderEmbedding` `Submodule` `Algebra.toModule` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Submodule.instPartialOrder` `instFunLikeOrderEmbedding` `toSubmodule`	—	—
`rTensorBot_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Subalgebra` `SetLike.instMembership` `instSetLike` `TensorProduct` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `toSemiring` `instModuleSubtypeMem` `Algebra.TensorProduct.instSemiring` `algebra` `Algebra.TensorProduct.instAlgebra` `AlgEquiv.instFunLike` `AlgEquiv.symm` `rTensorBot` `TensorProduct.tmul` `OneMemClass.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddSubmonoidWithOneClass.toOneMemClass` `SubsemiringClass.addSubmonoidWithOneClass` `instSubsemiringClass`	—	—
`rTensorBot_tmul` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `TensorProduct` `Subalgebra` `SetLike.instMembership` `instSetLike` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `toSemiring` `instModuleSubtypeMem` `Algebra.TensorProduct.instSemiring` `algebra` `Algebra.TensorProduct.instAlgebra` `AlgEquiv.instFunLike` `rTensorBot` `TensorProduct.tmul` `RingHom` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap` `Algebra.toSMul`	—	`Submodule.rTensorOne_tmul`
`rTensorBot_tmul_one` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `TensorProduct` `Subalgebra` `SetLike.instMembership` `instSetLike` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `toSemiring` `instModuleSubtypeMem` `Algebra.TensorProduct.instSemiring` `algebra` `Algebra.TensorProduct.instAlgebra` `AlgEquiv.instFunLike` `rTensorBot` `TensorProduct.tmul` `OneMemClass.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddSubmonoidWithOneClass.toOneMemClass` `SubsemiringClass.addSubmonoidWithOneClass` `instSubsemiringClass`	—	`Submodule.rTensorOne_tmul_one`
`val_mulMap'_tmul` 📖	mathematical	—	`Subalgebra` `CommSemiring.toSemiring` `SetLike.instMembership` `instSetLike` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Algebra.instCompleteLatticeSubalgebra` `DFunLike.coe` `AlgHom` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `toSemiring` `instModuleSubtypeMem` `Algebra.TensorProduct.instSemiring` `algebra` `Algebra.TensorProduct.instAlgebra` `AlgHom.funLike` `mulMap'` `TensorProduct.tmul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	—

---

← Back to Index