AlgebraicCurve.Place.le_ord_iff_mem_pow_fiberCenter
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_le_ord_iff_mem_pow_fiberCenter
open IsDedekindDomain WithZero IsLocalRing AlgebraicCurve AlgebraicCurve.PlaceLean source · statement
theorem _root_.AlgebraicCurve.Place.le_ord_iff_mem_pow_fiberCenter {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)
{c : integralClosureAt F' v} (hc : c ≠ 0) (n : ℕ) :
(n : ℤ) ≤ w.ord (algebraMap (integralClosureAt F' v) F' c) ↔
c ∈ (fiberCenter F' v hw).asIdeal ^ n