AlgebraicCurve.Place.restrictAlong_restrictAlong
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_restrictAlong_restrictAlong
open IsDedekindDomain AlgebraicCurveLean source · statement
theorem _root_.AlgebraicCurve.Place.restrictAlong_restrictAlong {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'') : (W.restrictAlong χ hχ).restrictAlong φ hφ =
W.restrictAlong (χ.comp φ) hχφ