AlgebraicCurve.Place.count_normalizedFactors_span_singleton
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_count_normalizedFactors_span_singleton
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid AlgebraicCurve
AlgebraicCurve.PlaceLean source · statement
theorem _root_.AlgebraicCurve.Place.count_normalizedFactors_span_singleton {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) :
(normalizedFactors (Ideal.span {c})).count (fiberCenter F' v hw).asIdeal
= (w.ord (algebraMap (integralClosureAt F' v) F' c)).toNat