Theorem: Encodable.encode_fintypeArrow (Logic/Vorspiel/Computability.lean)

State before:
β✝ : Type u_1
inst✝⁴ : Encodable β✝
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : Primcodable ι
inst✝¹ : DecidableEq ι
β : Type u_3
inst✝ : Primcodable β
f : ι → β
⊢ encode f = encode (fintypeArrowEquivFinArrow f)
Tactic:
rw[Encodable.encode_ofEquiv]
State after:
no goals