AlgebraicCurves.Places.Proofs.PlaceExistsComapToValuation.AlgebraicCurve.Place.rowMain
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceExistsComapToValuation
open IsDedekindDomain
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F']
[Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
[FiniteDimensional F F'] [Algebra.IsSeparable F F']Lean source · statement
theorem rowMain (v : Place K F) :
∃ w : Place K F', w.toValuationSubring.comap (algebraMap F F') = v.toValuationSubring