fin 0 → false

Stream: new members

[Heather Macbeth]

What's the right way to prove this? (I give a method which seems like the wrong way.)

import data.equiv.fin

example : fin 0 → false := equiv.false_equiv_empty.symm ∘ fin_zero_equiv

[Kenny Lau]

fin.elim0

[Yakov Pechersky]

What's the guidance in using fin.elim0 over fin_zero_elim?

[Eric Wieser]

One eliminates to things other than false, right?

[Eric Wieser]

docs#fin.elim0, docs#fin_zero_elim

[Eric Wieser]

Ah, one is mathlib the other is core, they're otherwise identical

[Yakov Pechersky]

Then I don't understand the docstring

[Eric Wieser]

#2055 gives some history

[Yakov Pechersky]

Ah, backward compat