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.

@[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.

Equations

• One or more equations did not get rendered due to their size.

@[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.

Equations

• One or more equations did not get rendered due to their size.

@[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.

Equations

• FunLike.distrib = Function.Injective.distrib (fun (f : F) => ⇑f) ⋯ ⋯ ⋯

@[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.

Equations

• FunLike.hasDistribNeg = Function.Injective.hasDistribNeg (fun (f : F) => ⇑f) ⋯ ⋯ ⋯

@[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.

Equations

• FunLike.addMonoidWithOne = Function.Injective.addMonoidWithOne (fun (f : F) => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[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.

Equations

• FunLike.addGroupWithOne = Function.Injective.addGroupWithOne (fun (f : F) => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[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.

Equations

• FunLike.nonUnitalNonAssocSemiring = Function.Injective.nonUnitalNonAssocSemiring (fun (f : F) => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯

@[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.

Equations

• FunLike.nonUnitalSemiring = Function.Injective.nonUnitalSemiring (fun (f : F) => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯

@[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.

Equations

• FunLike.nonAssocSemiring = Function.Injective.nonAssocSemiring (fun (f : F) => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[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.

Equations

• FunLike.semiring = Function.Injective.semiring (fun (f : F) => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[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.

Equations

• FunLike.nonUnitalCommSemiring = Function.Injective.nonUnitalCommSemiring (fun (f : F) => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯

@[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.

Equations

• FunLike.commSemiring = Function.Injective.commSemiring (fun (f : F) => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[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.

Equations

• FunLike.nonUnitalNonAssocRing = Function.Injective.nonUnitalNonAssocRing (fun (f : F) => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[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.

Equations

• FunLike.nonUnitalRing = Function.Injective.nonUnitalRing (fun (f : F) => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[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.

Equations

• FunLike.nonAssocRing = Function.Injective.nonAssocRing (fun (f : F) => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[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.

Equations

• FunLike.ring = Function.Injective.ring (fun (f : F) => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[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.

Equations

• FunLike.nonUnitalCommRing = Function.Injective.nonUnitalCommRing (fun (f : F) => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[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.

Equations

• FunLike.commRing = Function.Injective.commRing (fun (f : F) => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯