Zulip Chat Archive

Stream: new members

Topic: Is fin injective?


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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