Ring instances for FunLike types #
In this file we define various instances related to ring for FunLike types.
Note that currently, these are not registered as instances, but only abbrevs to avoid long
typeclass searches.
@[reducible, inline]
abbrev
FunLike.monoidWithZero
{F : Type u_1}
{α : Type u_2}
[FunLike F α α]
[Zero F]
[One F]
[Mul F]
[Zero α]
[IsZeroApply F α α]
[IsOneApplyEqSelf F α]
[IsMulApplyEqComp F α]
[ZeroHomClass 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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
abbrev
FunLike.semiring
{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]
[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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
abbrev
FunLike.ring
{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]
[IsNatCastApply F α]
[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.
Equations
- One or more equations did not get rendered due to their size.