AlgebraicCurve.Place.neg_log_valuation_fiberCenter_eq_ord
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_neg_log_valuation_fiberCenter_eq_ord
open IsDedekindDomain WithZero IsLocalRing AlgebraicCurve AlgebraicCurve.PlaceLean source · statement
theorem _root_.AlgebraicCurve.Place.neg_log_valuation_fiberCenter_eq_ord {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'] {v : Place K F} {w : Place K F'} (hw :
w.restrict F = v) {x : F'} (hx : x ≠ 0) :
-log ((fiberCenter F' v hw).valuation F' x) = w.ord x