AlgebraicCurve.Place.isRational_of_isAlgClosed
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_isRational_of_isAlgClosed
open AlgebraicCurve PolynomialLean source · statement
theorem _root_.AlgebraicCurve.Place.isRational_of_isAlgClosed {K F : Type*} [Field K] [IsAlgClosed
K] [Field F] [Algebra K F] [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F]
[FiniteDimensional (RatFunc K) F] (v : Place K F) : v.IsRational