LeanPool.FormalizationOfBoundedArithmetic.Algebra

theorem isAddRightRegular_one {M : Type u} [iopen : IOPENModel M] : IsAddRightRegular 1

instance instIsRightCancelAdd_leanPool {M : Type u} [iopen : IOPENModel M] : IsRightCancelAdd M

@[implicit_reducible]

instance instMulZeroClassLeanPool {M : Type u} [iopen : IOPENModel M] : MulZeroClass M

Equations

• instMulZeroClassLeanPool = { toMul := FirstOrder.Language.peano.instMulOfStructure, toZero := FirstOrder.Language.peano.instZeroOfStructure, zero_mul := ⋯, mul_zero := ⋯ }

@[implicit_reducible]

instance instCommMonoidLeanPool {M : Type u} [iopen : IOPENModel M] : CommMonoid M

Equations

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

@[implicit_reducible]

instance instAddCommMonoidLeanPool {M : Type u} [iopen : IOPENModel M] : AddCommMonoid M

Equations

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

@[implicit_reducible]

instance instSemiringLeanPool {M : Type u} [iopen : IOPENModel M] : Semiring M

Equations

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

instance instIsOrderedAddMonoid_leanPool {M : Type u} [idelta0 : IDelta0Model M] : IsOrderedAddMonoid M

instance instIsOrderedMonoid_leanPool {M : Type u} [idelta0 : IDelta0Model M] : IsOrderedMonoid M

@[implicit_reducible]

instance instAddCommMonoidLeanPool' {M : Type u} [idelta0 : IDelta0Model M] : AddCommMonoid M

Equations

• instAddCommMonoidLeanPool' = { toAddMonoid := instSemiringLeanPool.toNonAssocSemiring.toAddCommMonoidWithOne.toAddMonoid, add_comm := ⋯ }

instance instIsOrderedRing_leanPool {M : Type u} [idelta0 : IDelta0Model M] : IsOrderedRing M

@[implicit_reducible]

instance instCommSemiringLeanPool {M : Type u} [idelta0 : IDelta0Model M] : CommSemiring M

Equations

• instCommSemiringLeanPool = { toSemiring := instSemiringLeanPool, mul_comm := ⋯ }

instance instIsLeftCancelAdd_leanPool {M : Type u} [idelta0 : IDelta0Model M] : IsLeftCancelAdd M