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_reducible]

instance Fintype.decidableEqMulEquivFintype {α : Type u_3} {β : Type u_4} [DecidableEq β] [Fintype α] [Mul α] [Mul β] : DecidableEq (α ≃* β)

Equations

• Fintype.decidableEqMulEquivFintype a b = decidable_of_iff (⇑a = ⇑b) ⋯

@[instance_reducible]

instance Fintype.decidableEqAddEquivFintype {α : Type u_3} {β : Type u_4} [DecidableEq β] [Fintype α] [Add α] [Add β] : DecidableEq (α ≃+ β)

Equations

• Fintype.decidableEqAddEquivFintype a b = decidable_of_iff (⇑a = ⇑b) ⋯