AlgebraicCurve.Pic0.zsmul_mk
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_zsmul_mk
open AlgebraicCurveLean source · statement
theorem _root_.AlgebraicCurve.Pic0.zsmul_mk {K F : Type*} [Field K] [Field F] [Algebra K F] (m : ℤ)
(D : Divisor.degZero (K := K) (F := F)) : m • Pic0.mk D = Pic0.mk (m • D)