AlgebraicCurve.Place.deg_eq_one_of_isAlgClosed
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_deg_eq_one_of_isAlgClosed
open AlgebraicCurveLean source · statement
theorem _root_.AlgebraicCurve.Place.deg_eq_one_of_isAlgClosed {K F : Type*} [Field K] [Field F]
[Algebra K F] [IsAlgClosed K] (v : Place K F) (hv : v.deg ≠ 0) : v.deg = 1