Documentation
Seymour
.
Mathlib
.
ZMod
Search
Google site search
return to top
source
Imports
Init
Mathlib.Data.ZMod.Defs
Imported by
Z2_eq_1_of_ne_0
source
theorem
Z2_eq_1_of_ne_0
{a :
ZMod
2
}
(ha :
a
≠
0
)
:
a
=
1