English
Let x ∈ L and p ∈ K[X] with aeval x p = 0 and p.coeff 0 ≠ 0. Then x⁻¹ equals the negative of aeval x (divX p) divided by p.coeff 0, up to the algebra map.
Русский
Пусть x ∈ L, p ∈ K[X], aeval x p = 0, и p(0) ≠ 0. Тогда x⁻¹ = −(aeval_x(divX p)) / (algebraMap_K L(p(0))).
LaTeX
$$$\\text{aeval}_x(p) = 0 \\land p(0) \\neq 0 \\Rightarrow x^{-1} = -\\dfrac{\\text{aeval}_x(\\operatorname{divX} p)}{\\operatorname{algebraMap}(K,L)(p(0))}$$$
Lean4
theorem inv_eq_of_root_of_coeff_zero_ne_zero {x : L} {p : K[X]} (aeval_eq : aeval x p = 0)
(coeff_zero_ne : p.coeff 0 ≠ 0) : x⁻¹ = -(aeval x (divX p) / algebraMap _ _ (p.coeff 0)) :=
by
convert
inv_eq_of_aeval_divX_ne_zero (p := p) (L := L) (mt (fun h => (algebraMap K L).injective ?_) coeff_zero_ne) using 1
· rw [aeval_eq, zero_sub, div_neg]
rw [RingHom.map_zero]
convert aeval_eq
conv_rhs => rw [← divX_mul_X_add p]
rw [map_add, map_mul, h, zero_mul, zero_add, aeval_C]
