theorem
L49 ↗exists_restrict_eq
AlgebraicCurve.Place.exists_restrict_eq
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_restrict_eq
noncomputable section
open _root_.AlgebraicCurve
open _root_.IsDedekindDomain
open scoped Pointwise
open _root_.AlgebraicCurve.Place
_root_.AlgebraicCurves.Places.Proofs.Place_exists_restrict_eq.AlgebraicCurve.Place inLean source · statement
theorem _root_.AlgebraicCurve.Place.exists_restrict_eq {K F' M : Type*} [Field K] [Field F']
[Field M]
[Algebra K F'] [Algebra K M] [Algebra F' M] [IsScalarTower K F' M]
[FiniteDimensional F' M] [Algebra.IsSeparable F' M] (w : Place K F') :
∃ W : Place K M, W.restrict F' = w