Cast of integers into fields #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
This file concerns the canonical homomorphism
ℤ → F, where
F is a field.
Main results #
Auxiliary lemma for norm_cast to move the cast
-↑n upwards to
(The restriction to
field is necessary, otherwise this would also apply in the case where
R = ℤ and cause nontermination.)