Structures · Algebra
TensorProduct.CompatibleSMul
A typeclass for SMul structures which can be moved across a tensor product.
This typeclass is generated automatically from an IsScalarTower instance, but exists so that
we can also add an instance for AddCommGroup.toIntModule, allowing z • to be moved even if
R does not support negation.
Note that Module R' (M ⊗[R] N) is available even without this typeclass on R'; it's only
needed if TensorProduct.smul_tmul, TensorProduct.smul_tmul', or TensorProduct.tmul_smul is
used.
- Defined in
- Mathlib.LinearAlgebra.TensorProduct.Defs
- Shape
- 4 explicit arguments · adds smul_tmul
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by23
- TensorProduct.tmul_smul
- TensorProduct.smul_tmul
- Algebra.TensorProduct.mapOfCompatibleSMul
- TensorProduct.mapOfCompatibleSMul
- Algebra.TensorProduct.lmulEquiv
- Algebra.TensorProduct.lidOfCompatibleSMul
- TensorProduct.CompatibleSMul.smul_tmul
- TensorProduct.mapOfCompatibleSMul_tmul
- Algebra.TensorProduct.equivOfCompatibleSMul
- TensorProduct.mapOfCompatibleSMul_surjective
- TensorProduct.equivOfCompatibleSMul
- TensorProduct.lidOfCompatibleSMul
- TensorProduct.isScalarTower_right
- Algebra.TensorProduct.lmulEquiv_eq_lidOfCompatibleSMul
- Algebra.TensorProduct.mapOfCompatibleSMul'
- Algebra.TensorProduct.mapOfCompatibleSMul.congr_simp
- TensorProduct.lidOfCompatibleSMul_tmul
- TensorProduct.mapOfCompatibleSMul'
- Algebra.TensorProduct.mapOfCompatibleSMul_tmul
- TensorProduct.CompatibleSMul.unit
- Algebra.TensorProduct.lidOfCompatibleSMul_tmul
- Algebra.TensorProduct.mapOfCompatibleSMul_surjective
- TensorProduct.mapOfCompatibleSMul.congr_simp
Ancestors0
No ancestors.