Theorems · Inductive type · group theory

SMulDistribClass

(G : Type u_9) → (R : Type u_10) → (S : Type u_11) → [SMul G R] → [SMul G S] → [SMul R S] → Prop

An instance of SMulDistribClass G R S states that the multiplicative action of G on S is determined by the multiplicative actions of G on R and R on S. This is similar to IsScalarTower except that the action of G distributes over the action of R on S. E.g. if M/L/K is a tower of galois extensions then SMulDistribClass Gal(M/K) L M.

Defined in

Mathlib.Algebra.Group.Action.Defs

Cited by

23 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

SMulSMulSMul