Module

Mem_repartitionsOf_iff_coe_mem_adeleBdd.lean

Nyll.AlgebraicCurves.Cohomology.Mem_repartitionsOf_iff_coe_mem_adeleBdd

1 declaration indexed from sourceView source ↗

Module documentation

Divisor-bounded repartitions are precisely the bounded adelic families for that divisor.

Imports3

Imported by3

theorem

mem_repartitionsOf_iff_coe_mem_adeleBdd

L37 ↗

AlgebraicCurve.mem_repartitionsOf_iff_coe_mem_adeleBdd

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs.Mem_repartitionsOf_iff_coe_mem_adeleBdd
open _root_.AlgebraicCurves.Cohomology.Proofs in
open _root_.AlgebraicCurve Mem_repartitionsOf_iff_coe_mem_adeleBdd.AlgebraicCurve WithZero in

Lean source · statement

theorem _root_.AlgebraicCurve.mem_repartitionsOf_iff_coe_mem_adeleBdd {K F : Type*} [Field K]
    [Field F] [Algebra K F] {D : Divisor K F} {α : ↥(repartitions K F)} :
    α ∈ repartitionsOf D ↔ (α : Place K F → F) ∈ adeleBdd D

Module documentation

Declarations

mem_repartitionsOf_iff_coe_mem_adeleBdd