## Stream: new members

### Topic: Is fin injective?

#### Walter Moreira (May 04 2020 at 03:43):

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 (May 04 2020 at 03:44):

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

#### Jalex Stark (May 04 2020 at 04:02):

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 (May 04 2020 at 04:50):

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 (May 04 2020 at 04:55):

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

Last updated: May 14 2021 at 21:11 UTC