AlgebraicCurve.mem_range_algebraMap_of_isAlgebraic
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Mem_range_algebraMap_of_isAlgebraicLean source · statement
theorem _root_.AlgebraicCurve.mem_range_algebraMap_of_isAlgebraic {K L : Type*} [Field K] [Field L]
[Algebra K L] [IsAlgClosed K] {x : L} (hx : IsAlgebraic K x) :
x ∈ (algebraMap K L).range