Finite types with addition/multiplications #
This file contains basic results and instances for finite types that have an addition/multiplication operator.
Main results #
Fintype.decidableEqMulEquivFintype:MulEquivs on finite types have decidable equality
instance
Fintype.decidableEqMulEquivFintype
{α : Type u_4}
{β : Type u_5}
[DecidableEq β]
[Fintype α]
[Mul α]
[Mul β]
:
DecidableEq (α ≃* β)
Equations
- Fintype.decidableEqMulEquivFintype a b = decidable_of_iff (⇑a = ⇑b) ⋯
instance
Fintype.decidableEqAddEquivFintype
{α : Type u_4}
{β : Type u_5}
[DecidableEq β]
[Fintype α]
[Add α]
[Add β]
:
DecidableEq (α ≃+ β)
Equations
- Fintype.decidableEqAddEquivFintype a b = decidable_of_iff (⇑a = ⇑b) ⋯