Theorems · Definition · ring theory

FunLike.ring

{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 : Neg F] →
                [inst_6 : Sub F] →
                  [inst_7 : AddCommGroup α] →
                    [IsZeroApply F α α] →
                      [IsAddApply F α α] →
                        [IsOneApplyEqSelf F α] →
                          [IsMulApplyEqComp F α] →
                            [IsNegApply F α α] →
                              [IsSubApply F α α] →
                                [inst_14 : SMul ℕ F] →
                                  [IsSMulApply ℕ F α α] →
                                    [inst_16 : SMul ℤ F] →
                                      [IsSMulApply ℤ F α α] →
                                        [AddMonoidHomClass F α α] →
                                          [inst_19 : NatCast F] →
                                            [IsNatCastApply F α] → [inst_21 : IntCast F] → [IsIntCastApply F α] → Ring F

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

Defined in

Mathlib.Data.FunLike.Ring

Cited by

0 results in Mathlib

Foundations

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

Assumes

FunLikeZeroOneMulAddNegSubAddCommGroupIsZeroApplyIsAddApplyIsOneApplyEqSelfIsMulApplyEqCompIsNegApplyIsSubApplySMulIsSMulApplySMulIsSMulApplyAddMonoidHomClassNatCastIsNatCastApplyIntCastIsIntCastApply