Integer casts that stay nonzero #
An even integer with nonzero cast keeps 2 nonzero: if 2 cast to the ring were zero then so
would be the cast of anything 2 divides.
Nonvanishing of the cast is all that is claimed. In a general ring that is weaker than the cast
being a unit, and it is the form a hypothesis like (n : R) ≠ 0 on an index actually takes: at
even n it yields (2 : R) ≠ 0.
theorem
Int.two_ne_zero_of_even_of_cast_ne_zero
{R : Type u_1}
[NonAssocRing R]
{n : ℤ}
(heven : Even n)
(h : ↑n ≠ 0)
:
An even integer whose cast is nonzero forces the cast of 2 to be nonzero: it is 2 times
something, so a vanishing 2 would make it vanish too.