Theorems · Theorem · group theory

MulSemiringActionSemiHomClass.toMonoidHomClass

∀ {F : Type u_15} {M : outParam (Type u_16)} {N : outParam (Type u_17)} {inst : Monoid M} {inst_1 : Monoid N}
  {φ : outParam (M → N)} {R : outParam (Type u_18)} {S : outParam (Type u_19)} {inst_2 : Semiring R}
  {inst_3 : Semiring S} {inst_4 : DistribMulAction M R} {inst_5 : DistribMulAction N S} {inst_6 : FunLike F R S}
  [self : MulSemiringActionSemiHomClass F φ R S], MonoidHomClass F R S

Defined in: Mathlib.GroupTheory.GroupAction.Hom
Cited by: 0 results in Mathlib
Foundations: Depth 12 from the axioms · uses no axioms
Assumes: MulSemiringActionSemiHomClass

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Semiringstatement and proof · cited by 13,802
Monoidstatement and proof · cited by 3,887
FunLikestatement and proof · cited by 2,560
DistribMulActionstatement and proof · cited by 584
MonoidHomClassstatement · cited by 244
MulSemiringActionSemiHomClassstatement and proof · cited by 1

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.