Documentation

Mathlib.Algebra.Ring.FunLike

Ring instances for FunLike types #

In this file we define various instances related to ring for FunLike types. There are two different variants: either the multiplication is given by composition or it is pointwise multiplication.

Note that currently, these are not registered as instances, but only abbrevs to avoid long typeclass searches.

source
@[reducible, inline]
abbrev FunLike.compSemiring {F : Type u_1} {α : Type u_2} [FunLike F α α] [Zero F] [One F] [Mul F] [Add F] [AddCommMonoid α] [IsZeroApply F] [IsAddApply F] [IsOneApplyEqSelf F] [IsMulApplyEqComp F] [SMul ℕ F] [IsSMulApply ℕ F] [AddMonoidHomClass F α α] [NatCast F] [IsNatCastApplyEqSMul F] :
Semiring F

A FunLike type with (f * g) x = f (g x) is a Semiring.

Instances For
    source
    @[reducible, inline]
    abbrev FunLike.compRing {F : Type u_1} {α : Type u_2} [FunLike F α α] [Zero F] [One F] [Mul F] [Add F] [Neg F] [Sub F] [AddCommGroup α] [IsZeroApply F] [IsAddApply F] [IsOneApplyEqSelf F] [IsMulApplyEqComp F] [IsNegApply F] [IsSubApply F] [SMul ℕ F] [IsSMulApply ℕ F] [SMul ℤ F] [IsSMulApply ℤ F] [AddMonoidHomClass F α α] [NatCast F] [IsNatCastApplyEqSMul F] [IntCast F] [IsIntCastApplyEqSMul F] :
    Ring F

    A FunLike type with (f * g) x = f (g x) is a Ring.

    Instances For
      source
      @[reducible, inline]
      abbrev FunLike.distrib {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Add F] [Mul F] [Distrib β] [IsAddApply F] [IsMulApply F] :
      Distrib F

      A FunLike type with (f * g) x = f x * g x is a Distrib if β is a Distrib.

      Instances For
        source
        @[reducible, inline]
        abbrev FunLike.hasDistribNeg {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Neg F] [Mul F] [Mul β] [HasDistribNeg β] [IsNegApply F] [IsMulApply F] :
        HasDistribNeg F

        A FunLike type with (f * g) x = f x * g x is a HasDistribNeg if β is a HasDistribNeg.

        Instances For
          source
          @[reducible, inline]
          abbrev FunLike.addMonoidWithOne {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Zero F] [One F] [Add F] [SMul ℕ F] [NatCast F] [AddMonoidWithOne β] [IsZeroApply F] [IsOneApply F] [IsAddApply F] [IsSMulApply ℕ F] [IsNatCastApply F] :
          AddMonoidWithOne F

          A FunLike type with (f * g) x = f x * g x is an AddMonoidWithOne if β is an AddMonoidWithOne.

          Instances For
            source
            @[reducible, inline]
            abbrev FunLike.addGroupWithOne {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Zero F] [One F] [Add F] [Neg F] [Sub F] [SMul ℕ F] [SMul ℤ F] [NatCast F] [IntCast F] [AddGroupWithOne β] [IsZeroApply F] [IsOneApply F] [IsAddApply F] [IsNegApply F] [IsSubApply F] [IsSMulApply ℕ F] [IsSMulApply ℤ F] [IsNatCastApply F] [IsIntCastApply F] :
            AddGroupWithOne F

            A FunLike type with (f * g) x = f x * g x is an AddGroupWithOne if β is an AddGroupWithOne.

            Instances For
              source
              @[reducible, inline]
              abbrev FunLike.nonUnitalNonAssocSemiring {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Zero F] [Add F] [Mul F] [SMul ℕ F] [NonUnitalNonAssocSemiring β] [IsZeroApply F] [IsAddApply F] [IsMulApply F] [IsSMulApply ℕ F] :
              NonUnitalNonAssocSemiring F

              A FunLike type with (f * g) x = f x * g x is a NonUnitalNonAssocSemiring if β is a NonUnitalNonAssocSemiring.

              Instances For
                source
                @[reducible, inline]
                abbrev FunLike.nonUnitalSemiring {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Zero F] [Add F] [Mul F] [SMul ℕ F] [NonUnitalSemiring β] [IsZeroApply F] [IsAddApply F] [IsMulApply F] [IsSMulApply ℕ F] :
                NonUnitalSemiring F

                A FunLike type with (f * g) x = f x * g x is a NonUnitalSemiring if β is a NonUnitalSemiring.

                Instances For
                  source
                  @[reducible, inline]
                  abbrev FunLike.nonAssocSemiring {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Zero F] [One F] [Add F] [Mul F] [SMul ℕ F] [NatCast F] [NonAssocSemiring β] [IsZeroApply F] [IsOneApply F] [IsAddApply F] [IsMulApply F] [IsSMulApply ℕ F] [IsNatCastApply F] :
                  NonAssocSemiring F

                  A FunLike type with (f * g) x = f x * g x is a NonAssocSemiring if β is a NonAssocSemiring.

                  Instances For
                    source
                    @[reducible, inline]
                    abbrev FunLike.semiring {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Zero F] [One F] [Add F] [Mul F] [SMul ℕ F] [Pow F ℕ] [NatCast F] [Semiring β] [IsZeroApply F] [IsOneApply F] [IsAddApply F] [IsMulApply F] [IsSMulApply ℕ F] [IsPowApply ℕ F] [IsNatCastApply F] :
                    Semiring F

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

                    Instances For
                      source
                      @[reducible, inline]
                      abbrev FunLike.nonUnitalCommSemiring {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Zero F] [Add F] [Mul F] [SMul ℕ F] [NonUnitalCommSemiring β] [IsZeroApply F] [IsAddApply F] [IsMulApply F] [IsSMulApply ℕ F] :
                      NonUnitalCommSemiring F

                      A FunLike type with (f * g) x = f x * g x is a NonUnitalCommSemiring if β is a NonUnitalCommSemiring.

                      Instances For
                        source
                        @[reducible, inline]
                        abbrev FunLike.commSemiring {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Zero F] [One F] [Add F] [Mul F] [SMul ℕ F] [Pow F ℕ] [NatCast F] [CommSemiring β] [IsZeroApply F] [IsOneApply F] [IsAddApply F] [IsMulApply F] [IsSMulApply ℕ F] [IsPowApply ℕ F] [IsNatCastApply F] :
                        CommSemiring F

                        A FunLike type with (f * g) x = f x * g x is a CommSemiring if β is a CommSemiring.

                        Instances For
                          source
                          @[reducible, inline]
                          abbrev FunLike.nonUnitalNonAssocRing {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Zero F] [Add F] [Neg F] [Sub F] [Mul F] [SMul ℕ F] [SMul ℤ F] [NonUnitalNonAssocRing β] [IsZeroApply F] [IsAddApply F] [IsMulApply F] [IsNegApply F] [IsSubApply F] [IsSMulApply ℕ F] [IsSMulApply ℤ F] :
                          NonUnitalNonAssocRing F

                          A FunLike type with (f * g) x = f x * g x is a NonUnitalNonAssocRing if β is a NonUnitalNonAssocRing.

                          Instances For
                            source
                            @[reducible, inline]
                            abbrev FunLike.nonUnitalRing {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Zero F] [Add F] [Neg F] [Sub F] [Mul F] [SMul ℕ F] [SMul ℤ F] [NonUnitalRing β] [IsZeroApply F] [IsAddApply F] [IsMulApply F] [IsNegApply F] [IsSubApply F] [IsSMulApply ℕ F] [IsSMulApply ℤ F] :
                            NonUnitalRing F

                            A FunLike type with (f * g) x = f x * g x is a NonUnitalRing if β is a NonUnitalRing.

                            Instances For
                              source
                              @[reducible, inline]
                              abbrev FunLike.nonAssocRing {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Zero F] [One F] [Add F] [Neg F] [Sub F] [Mul F] [SMul ℕ F] [SMul ℤ F] [NatCast F] [IntCast F] [NonAssocRing β] [IsZeroApply F] [IsOneApply F] [IsAddApply F] [IsMulApply F] [IsNegApply F] [IsSubApply F] [IsSMulApply ℕ F] [IsSMulApply ℤ F] [IsNatCastApply F] [IsIntCastApply F] :
                              NonAssocRing F

                              A FunLike type with (f * g) x = f x * g x is a NonAssocRing if β is a NonAssocRing.

                              Instances For
                                source
                                @[reducible, inline]
                                abbrev FunLike.ring {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Zero F] [One F] [Add F] [Neg F] [Sub F] [Mul F] [SMul ℕ F] [SMul ℤ F] [Pow F ℕ] [NatCast F] [IntCast F] [Ring β] [IsZeroApply F] [IsOneApply F] [IsAddApply F] [IsMulApply F] [IsNegApply F] [IsSubApply F] [IsSMulApply ℕ F] [IsSMulApply ℤ F] [IsPowApply ℕ F] [IsNatCastApply F] [IsIntCastApply F] :
                                Ring F

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

                                Instances For
                                  source
                                  @[reducible, inline]
                                  abbrev FunLike.nonUnitalCommRing {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Zero F] [Add F] [Neg F] [Sub F] [Mul F] [SMul ℕ F] [SMul ℤ F] [NonUnitalCommRing β] [IsZeroApply F] [IsAddApply F] [IsMulApply F] [IsNegApply F] [IsSubApply F] [IsSMulApply ℕ F] [IsSMulApply ℤ F] :
                                  NonUnitalCommRing F

                                  A FunLike type with (f * g) x = f x * g x is a NonUnitalCommRing if β is a NonUnitalCommRing.

                                  Instances For
                                    source
                                    @[reducible, inline]
                                    abbrev FunLike.commRing {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Zero F] [One F] [Add F] [Neg F] [Sub F] [Mul F] [SMul ℕ F] [SMul ℤ F] [Pow F ℕ] [NatCast F] [IntCast F] [CommRing β] [IsZeroApply F] [IsOneApply F] [IsAddApply F] [IsMulApply F] [IsNegApply F] [IsSubApply F] [IsSMulApply ℕ F] [IsSMulApply ℤ F] [IsPowApply ℕ F] [IsNatCastApply F] [IsIntCastApply F] :
                                    CommRing F

                                    A FunLike type with (f * g) x = f x * g x is a CommRing if β is a CommRing.

                                    Instances For