Documentation
Mathlib
.
Init
.
Data
.
Fin
.
Basic
Search
Google site search
return to top
source
Imports
Init
Mathlib.Init.Data.Nat.Notation
Imported by
Fin
.
eq_of_veq
Fin
.
veq_of_eq
Fin
.
ne_of_vne
Fin
.
vne_of_ne
Theorems about equality in
Fin
.
#
source
@[deprecated Fin.eq_of_val_eq]
theorem
Fin
.
eq_of_veq
{n :
ℕ
}
{i :
Fin
n
}
{j :
Fin
n
}
:
↑
i
=
↑
j
→
i
=
j
source
@[deprecated Fin.val_eq_of_eq]
theorem
Fin
.
veq_of_eq
{n :
ℕ
}
{i :
Fin
n
}
{j :
Fin
n
}
:
i
=
j
→
↑
i
=
↑
j
source
theorem
Fin
.
ne_of_vne
{n :
ℕ
}
{i :
Fin
n
}
{j :
Fin
n
}
(h :
↑
i
≠
↑
j
)
:
i
≠
j
source
theorem
Fin
.
vne_of_ne
{n :
ℕ
}
{i :
Fin
n
}
{j :
Fin
n
}
(h :
i
≠
j
)
:
↑
i
≠
↑
j