Documentation

Mathlib.Algebra.Order.Monoid.Prod

Products of ordered monoids #

Equations
Equations
Equations
Equations
theorem Prod.instExistsMulOfLE {α : Type u_1} {β : Type u_2} [LE α] [LE β] [Mul α] [Mul β] [ExistsMulOfLE α] [ExistsMulOfLE β] :
theorem Prod.instExistsAddOfLE {α : Type u_1} {β : Type u_2} [LE α] [LE β] [Add α] [Add β] [ExistsAddOfLE α] [ExistsAddOfLE β] :
Equations
Equations
Equations
Equations
Equations
Equations