Theorems · Theorem · group theory

FaithfulVAdd.trans

∀ (R : Type u_4) (S : Type u_5) (T : Type u_6) [inst : AddMonoid S] [inst_1 : AddZeroClass T] [inst_2 : VAdd R S]
  [VAddAssocClass R S S] [inst_4 : AddAction S T] [VAddAssocClass S T T] [inst_6 : VAdd R T] [VAddAssocClass R T T]
  [VAddAssocClass R S T] [FaithfulVAdd R S] [FaithfulVAdd S T], FaithfulVAdd R T

Defined in

Mathlib.Algebra.Group.Action.Faithful

Cited by

0 results in Mathlib

Foundations

Depth 9 from the axioms · uses propext, Quot.sound

Assumes

AddMonoidAddZeroClassVAddVAddAssocClassAddActionVAddAssocClassVAddVAddAssocClassVAddAssocClassFaithfulVAddFaithfulVAdd