English
If two quadratic characters χ, χ' with target ℤ have equal values after embedding into a ring with characteristic not equal to 2, then χ(a) = χ'(a') in ℤ.
Русский
Если два квадратичных характера χ, χ' с целью ℤ принимают равные значения после их вложения в кольцо с характеристикой не равной 2, тогда χ(a) = χ'(a') в ℤ.
LaTeX
$$$$ χ a = χ' a' \\text{ in } \\mathbb{Z} \\;\\Longrightarrow\\; χ a = χ' a' \\; (under the given embedding and } \\operatorname{ringChar}(R'') \\neq 2). $$$$
Lean4
/-- If two values of quadratic characters with target `ℤ` agree after coercion into a ring
of characteristic not `2`, then they agree in `ℤ`. -/
theorem eq_of_eq_coe {χ : MulChar R ℤ} (hχ : IsQuadratic χ) {χ' : MulChar R' ℤ} (hχ' : IsQuadratic χ') [Nontrivial R'']
(hR'' : ringChar R'' ≠ 2) {a : R} {a' : R'} (h : (χ a : R'') = χ' a') : χ a = χ' a' :=
Int.cast_injOn_of_ringChar_ne_two hR'' (hχ a) (hχ' a') h
