Theorems · Definition · ring theory

FunLike.monoidWithZero

{F : Type u_1} →
  {α : Type u_2} →
    [inst : FunLike F α α] →
      [inst_1 : Zero F] →
        [inst_2 : One F] →
          [inst_3 : Mul F] →
            [inst_4 : Zero α] →
              [IsZeroApply F α α] →
                [IsOneApplyEqSelf F α] → [IsMulApplyEqComp F α] → [ZeroHomClass F α α] → MonoidWithZero F

A FunLike type with (f + g) x = f x + g x and (f * g) x = f (g x) is a MonoidWithZero if α is a MonoidWithZero.

Defined in

Mathlib.Data.FunLike.Ring

Cited by

0 results in Mathlib

Foundations

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

Assumes

FunLikeZeroOneMulZeroIsZeroApplyIsOneApplyEqSelfIsMulApplyEqCompZeroHomClass