Documentation
ForbiddenMatrix
.
Mathlib
.
Data
.
ZMod
.
Basic
Search
return to top
source
Imports
Init
Mathlib.Data.ZMod.Basic
Imported by
Fin
.
natCast_val_eq_zmodFinEquiv
source
@[simp]
theorem
Fin
.
natCast_val_eq_zmodFinEquiv
{
n
:
ℕ
}
[
NeZero
n
]
(
a
:
Fin
n
)
:
↑
↑
a
=
(
ZMod.finEquiv
n
)
a