English
Let x ∈ L and p ∈ K[X] with aeval x (divX p) ≠ 0. Then x⁻¹ equals aeval x (divX p) divided by (aeval x p − algebraMap_K L (p.coeff 0)).
Русский
Пусть x ∈ L, p ∈ K[X], и aeval_x(divX p) ≠ 0. Тогда x⁻¹ = aeval_x(divX p) / (aeval_x(p) − algebraMap_K L(p(0))).
LaTeX
$$$\\text{aeval}_x(\\operatorname{divX} p) \\neq 0 \\;\Rightarrow\; x^{-1} = \\dfrac{\\text{aeval}_x(\\operatorname{divX} p)}{\\text{aeval}_x(p) - \\operatorname{algebraMap}(K,L)(p(0))}$$$
Lean4
theorem inv_eq_of_aeval_divX_ne_zero {x : L} {p : K[X]} (aeval_ne : aeval x (divX p) ≠ 0) :
x⁻¹ = aeval x (divX p) / (aeval x p - algebraMap _ _ (p.coeff 0)) :=
by
rw [inv_eq_iff_eq_inv, inv_div, eq_comm, div_eq_iff, sub_eq_iff_eq_add, mul_comm]
conv_lhs => rw [← divX_mul_X_add p]
· rw [map_add, map_mul, aeval_X, aeval_C]
· exact aeval_ne
