Theorems · Inductive type · nonassociative algebras

NonUnitalAlgSemiHomClass

(F : Type u_1) →
  {R : outParam (Type u_2)} →
    {S : outParam (Type u_3)} →
      [inst : Monoid R] →
        [inst_1 : Monoid S] →
          outParam (R →* S) →
            (A : outParam (Type u_4)) →
              (B : outParam (Type u_5)) →
                [inst_2 : NonUnitalNonAssocSemiring A] →
                  [inst_3 : NonUnitalNonAssocSemiring B] →
                    [DistribMulAction R A] → [DistribMulAction S B] → [FunLike F A B] → Prop

NonUnitalAlgSemiHomClass F φ A B asserts F is a type of bundled algebra homomorphisms from A to B which are equivariant with respect to φ.

Defined in

Mathlib.Algebra.Algebra.NonUnitalHom

Cited by

1 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

MonoidMonoidNonUnitalNonAssocSemiringNonUnitalNonAssocSemiringDistribMulActionDistribMulActionFunLike