Structures · Algebra
IsScalarTower
An instance of IsScalarTower M N α states that the multiplicative
action of M on α is determined by the multiplicative actions of M on N
and N on α.
- Defined in
- Mathlib.Algebra.Group.Action.Defs
- Shape
- 3 explicit arguments · adds smul_assoc
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by5
Concrete types that are instances34
- Int
- Nat
- Real
- Rat
- NNReal
- ZMod
- Polynomial
- Padic
- CommRingCat.carrier
- RatFunc
- NNRat
- FractionRing
- WithVal
- Units
- IsLocalRing.ResidueField
- NumberField.RingOfIntegers
- Algebra.Presentation.Core
- CentroidHom
- IncidenceAlgebra
- Circle
- Complex.UnitClosedDisc
- Localization.AtPrime
- Algebra.Generators.Ring
- Subtype
- OrderDual
- Set.Elem
- ULift
- MulOpposite
- PUnit
- Lex
- WithAbs
- Set
- Finset
- Filter
How is a type an instance?
Loading the hierarchy index…
Assumed by4,794
- IsScalarTower.toAlgHom
- cfcₙ
- Submodule.restrictScalars
- TensorProduct.AlgebraTensorModule.curry_injective
- smul_assoc
- ContinuousLinearMap.smulRight
- TensorProduct.AlgebraTensorModule.curry_apply
- IsScalarTower.algebraMap_apply
- IsScalarTower.algebraMap_eq
- Algebra.TensorProduct.map
- algebraMap_smul
- IsBaseChange
- AlgHom.restrictScalars
- CFC.sqrt
- IntermediateField.LinearDisjoint
- TensorProduct.AlgebraTensorModule.curry
- smul_mul_assoc
- ContinuousLinearMap.lsmul
- IntermediateField.restrictScalars
- cfcₙHom
- ContinuousLinearMap.mul
- LinearMap.mul
- AlgEquiv.restrictScalars
- LinearMap.smulRight
- Algebra.Generators.comp
- DoubleCentralizer.toProd
- LinearMap.mul'
- Algebra.TensorProduct.lift
- LinearMap.compr₂
- smul_one_smul
- NonUnitalStarAlgebra.adjoin
- CFC.abs
- SMulCommClass.of_commMonoid
- Algebra.Extension.Cotangent.map
- Submodule.localized'
- Algebra.Generators.Hom.toExtensionHom
- TensorProduct.AlgebraTensorModule.map
- Subalgebra.restrictScalars
- KaehlerDifferential.map
- QuadraticForm.tmul
- FractionalIdeal.dual
- NonUnitalAlgebra.adjoin
- TensorProduct.AlgebraTensorModule.cancelBaseChange
- Submodule.smul_mem_smul
- Algebra.Generators.ofComp
- cfcₙ_apply
- TensorProduct.AlgebraTensorModule.lTensor
- Polynomial.aeval_map_algebraMap
- IsIntegral.tower_top
- cfcₙ_apply_of_not_predicate
Ancestors0
No ancestors.