AlgebraicCurve.Place.ramificationIndexAlong_eq_of_pow_eq_of_isCoprime_ord
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ramificationIndexAlong_eq_of_pow_eq_of_isCoprime_ord
attribute [-instance]
AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
open AlgebraicCurveLean source · statement
theorem _root_.AlgebraicCurve.Place.ramificationIndexAlong_eq_of_pow_eq_of_isCoprime_ord
{k F F' : Type*} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F']
[AlgebraicCurve.HasPrincipalDivisors k F']
(φ : F →ₐ[k] F') (hφ : φ.toRingHom.IsIntegral)
(hfin : AlgebraicCurve.FiniteAlong k φ) (hsep : AlgebraicCurve.SeparableAlong k φ)
(n : ℕ) (hdeg : AlgebraicCurve.finrankAlong k φ = n)
(c : F') (u : F) (hu : φ u = c ^ n)
(P : AlgebraicCurve.Place k F')
(hcop : IsCoprime ((P.restrictAlong φ hφ).ord u) (n : ℤ)) :
P.ramificationIndexAlong φ = n