theorem
L24 ↗pullbackDiff_smul
AlgebraicCurve.pullbackDiff_smul
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.PullbackDiff_smul
open AlgebraicCurve inLean source · statement
theorem _root_.AlgebraicCurve.pullbackDiff_smul {K F F' : Type*} [Field K] [Field F] [Field F']
[Algebra K F] [Algebra K F'] (φ : F →ₐ[K] F') (g : F) (ω : Ω[F⁄K]) :
pullbackDiff φ (g • ω) = φ g • pullbackDiff φ ω