English
If Q ∈ A[X] has all coefficients divisible by p, and aeval x Q = p • z, then z lies in the adjoin of { x } inside A.
Русский
Если Q ∈ A[X] все коэффициенты делятся на p и aeval x Q = p • z, тогда z ∈ adjoin {x} внутри A.
LaTeX
$$$hp: p \\neq 0 \\to \\left( \\forall i, p \\mid Q.coeff i \\right) \\to aeval x Q = p \\cdot z \\to z \\in adjoin_A(\\{x\\})$$$
Lean4
theorem mem_adjoin_of_dvd_coeff_of_dvd_aeval {A B : Type*} [CommSemiring A] [Ring B] [Algebra A B]
[NoZeroSMulDivisors A B] {Q : A[X]} {p : A} {x z : B} (hp : p ≠ 0)
(hQ : ∀ i ∈ range (Q.natDegree + 1), p ∣ Q.coeff i) (hz : aeval x Q = p • z) : z ∈ adjoin A ({ x } : Set B) :=
by
choose! f hf using hQ
rw [aeval_eq_sum_range, sum_range] at hz
conv_lhs at hz =>
congr
next => skip
ext i
rw [hf i (mem_range.2 (Fin.is_lt i)), ← smul_smul]
rw [← smul_sum] at hz
rw [← smul_right_injective _ hp hz]
exact
Subalgebra.sum_mem _ fun _ _ =>
Subalgebra.smul_mem _ (Subalgebra.pow_mem _ (subset_adjoin (Set.mem_singleton _)) _) _
