Theorems · Definition · ring theory

FunLike.semiring

{F : Type u_1} →
  {α : Type u_2} →
    [inst : FunLike F α α] →
      [inst_1 : Zero F] →
        [inst_2 : One F] →
          [inst_3 : Mul F] →
            [inst_4 : Add F] →
              [inst_5 : AddCommMonoid α] →
                [IsZeroApply F α α] →
                  [IsAddApply F α α] →
                    [IsOneApplyEqSelf F α] →
                      [IsMulApplyEqComp F α] →
                        [inst_10 : SMul ℕ F] →
                          [IsSMulApply ℕ F α α] →
                            [AddMonoidHomClass F α α] → [inst_13 : NatCast F] → [IsNatCastApply F α] → Semiring F

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

Defined in

Mathlib.Data.FunLike.Ring

Cited by

0 results in Mathlib

Foundations

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

Assumes

FunLikeZeroOneMulAddAddCommMonoidIsZeroApplyIsAddApplyIsOneApplyEqSelfIsMulApplyEqCompSMulIsSMulApplyAddMonoidHomClassNatCastIsNatCastApply