Is fin injective?

Stream: new members

[Walter Moreira]

Hello folks. I'm a newbie to the forum. (Is it good etiquette to write an introduction? Or do those just add noise?)

Is it possible to prove fin n = fin m → n = m? I haven't seen propositions including the equality of fin types in the core library or mathlib, so I might be looking at this in the wrong way.

[Mario Carneiro]

This sort of proposition is almost never true, but it happens to be true for fin because card (fin n) = n

[Jalex Stark]

to flesh out what mario said,

import tactic
import data.finset

example {n m : ℕ} : fin m = fin n → m = n := begin
intro h,
have key : fintype.card (fin m) = fintype.card (fin n) := by cc,
simp only [fintype.card_fin] at key,
exact key,
end

[Johan Commelin]

Walter Moreira said:

Hello folks. I'm a newbie to the forum. (Is it good etiquette to write an introduction? Or do those just add noise?)

Welcome! Introductions are appreciated! Just start a new thread with your name as title, and tell us whatever you want. It's nice to meet new people!

[Walter Moreira]

Thanks @Mario Carneiro and @Jalex Stark! That makes total sense. (And thanks @Johan Commelin , I'll introduce myself in a different thread.)