Documentation
Init
.
Data
.
Prod
Search
Google site search
return to top
source
Imports
Init.SimpLemmas
Imported by
Init.Data.Nat.Linear
Init.Data
instLawfulBEqProd
source
instance
instLawfulBEqProd
{α :
Type
u_1}
{β :
Type
u_2}
[
BEq
α
]
[
BEq
β
]
[
LawfulBEq
α
]
[
LawfulBEq
β
]
:
LawfulBEq
(
α
×
β
)
Equations
⋯
=
⋯