English
If x ∈ A and x is algebraic over K, then x⁻¹ ∈ A.
Русский
Если x ∈ A и x алгебраичен над K, тогда x⁻¹ ∈ A.
LaTeX
$$$x \\in A \\,\\land\\, \\text{IsAlgebraic}\\; K\\; x \\Rightarrow x^{-1} \\in A$$$
Lean4
theorem inv_mem_of_algebraic {x : A} (hx : IsAlgebraic K (x : L)) : (x⁻¹ : L) ∈ A :=
by
obtain ⟨p, ne_zero, aeval_eq⟩ := hx
rw [Subalgebra.aeval_coe, Subalgebra.coe_eq_zero] at aeval_eq
revert ne_zero aeval_eq
refine p.recOnHorner ?_ ?_ ?_
· intro h
contradiction
· intro p a hp ha _ih _ne_zero aeval_eq
refine A.inv_mem_of_root_of_coeff_zero_ne_zero aeval_eq ?_
rwa [coeff_add, hp, zero_add, coeff_C, if_pos rfl]
· intro p hp ih _ne_zero aeval_eq
rw [map_mul, aeval_X, mul_eq_zero] at aeval_eq
rcases aeval_eq with aeval_eq | x_eq
· exact ih hp aeval_eq
· rw [x_eq, Subalgebra.coe_zero, inv_zero]
exact A.zero_mem
