Theorems · Inductive type · group theory

IsScalarTower

(M : Type u_9) → (N : Type u_10) → (α : Type u_11) → [SMul M N] → [SMul N α] → [SMul M α] → Prop

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

Cited by

3,896 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms

Assumes

SMulSMulSMul