AlgebraicCurve.Place.ramificationIndexAlong_comp
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ramificationIndexAlong_comp
open IsDedekindDomain AlgebraicCurveLean source · statement
theorem _root_.AlgebraicCurve.Place.ramificationIndexAlong_comp {K F F' F'' : Type*} [Field K]
[Field F] [Field F'] [Field F''] [Algebra K F] [Algebra K F'] [Algebra K F''] (φ : F →ₐ[K] F') (χ
: F' →ₐ[K] F'') (hφ : φ.toRingHom.IsIntegral) (hχ : χ.toRingHom.IsIntegral) (hχφ : (χ.comp
φ).toRingHom.IsIntegral) (W : Place K F'') : Place.ramificationIndexAlong (χ.comp φ) W =
Place.ramificationIndexAlong χ W * Place.ramificationIndexAlong φ (W.restrictAlong χ hχ)