AlgebraicCurve.Place.inertiaDegAlong_eq_one_of_isAlgClosed
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_inertiaDegAlong_eq_one_of_isAlgClosed
open AlgebraicCurveLean source · statement
theorem _root_.AlgebraicCurve.Place.inertiaDegAlong_eq_one_of_isAlgClosed
{K F F' : Type*} [Field K] [IsAlgClosed K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
[IsCurveOver K F] [Algebra.EssFiniteType K F] [IsCurveOver K F'] [Algebra.EssFiniteType K F']
(ψ : F →ₐ[K] F') (hψ : ψ.toRingHom.IsIntegral) (W : Place K F') :
W.inertiaDegAlong ψ hψ = 1