AlgebraicCurve.Place.restrict_eq_of_forall_mem
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_restrict_eq_of_forall_mem
noncomputable section
open _root_.AlgebraicCurveLean source · statement
theorem _root_.AlgebraicCurve.Place.restrict_eq_of_forall_mem {K F L : Type*} [Field K] [Field F]
[Field L]
[Algebra K F] [Algebra K L] [Algebra F L] [IsScalarTower K F L] [Algebra.IsIntegral F L]
(w : AlgebraicCurve.Place K F) (Q : AlgebraicCurve.Place K L)
(hQ : ∀ y ∈ w.toValuationSubring, algebraMap F L y ∈ Q.toValuationSubring) :
Q.restrict F = w