theorem
L26 ↗pullbackAlong_comp
AlgebraicCurve.Differential.pullbackAlong_comp
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Differential_pullbackAlong_comp
open AlgebraicCurve AlgebraicCurve.Differential KaehlerDifferentialLean source · statement
theorem _root_.AlgebraicCurve.Differential.pullbackAlong_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'') (ω : Ω[F⁄K]) :
AlgebraicCurve.Differential.pullbackAlong (ψ.comp φ) ω =
AlgebraicCurve.Differential.pullbackAlong ψ (AlgebraicCurve.Differential.pullbackAlong φ ω)