RamificationTheory.HilbertRamification.Higher.polynomial_eval₂_sub_mem_of_sub_mem
If two evaluation points are congruent modulo an ideal, then evaluating any polynomial at them gives congruent results modulo the same ideal.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace RamificationTheory.HilbertRamification
namespace HigherLean source · statement
theorem polynomial_eval₂_sub_mem_of_sub_mem
{R S : Type*} [CommRing R] [CommRing S]
(f : R →+* S) (I : Ideal S) {x y : S} (hxy : x - y ∈ I)
(P : Polynomial R) :
P.eval₂ f x - P.eval₂ f y ∈ I