structure ArakelovDivisor (K : Type u_1) [Field K] (hG : IsGlobalField K) : Type u_2

• val : IsGlobalField.PlaceType K → ℝ
• pos (v : IsGlobalField.PlaceType K) : 0 < self.val v
• finite_support : {v : IsGlobalField.PlaceType K | self.val v ≠ 1}.Finite

def ArakelovDivisor.one {K : Type u_1} [Field K] {hG : IsGlobalField K} : ArakelovDivisor K hG

def ArakelovDivisor.mul {K : Type u_1} [Field K] {hG : IsGlobalField K} (c d : ArakelovDivisor K hG) : ArakelovDivisor K hG

noncomputable def ArakelovDivisor.inv {K : Type u_1} [Field K] {hG : IsGlobalField K} (c : ArakelovDivisor K hG) : ArakelovDivisor K hG

@[implicit_reducible]

instance ArakelovDivisor.instOne {K : Type u_1} [Field K] {hG : IsGlobalField K} : One (ArakelovDivisor K hG)

@[implicit_reducible]

instance ArakelovDivisor.instMul {K : Type u_1} [Field K] {hG : IsGlobalField K} : Mul (ArakelovDivisor K hG)

@[implicit_reducible]

noncomputable instance ArakelovDivisor.instInv {K : Type u_1} [Field K] {hG : IsGlobalField K} : Inv (ArakelovDivisor K hG)

@[simp]

theorem ArakelovDivisor.one_val {K : Type u_1} [Field K] {hG : IsGlobalField K} (v : IsGlobalField.PlaceType K) : val 1 v = 1

@[simp]

theorem ArakelovDivisor.mul_val {K : Type u_1} [Field K] {hG : IsGlobalField K} (c d : ArakelovDivisor K hG) (v : IsGlobalField.PlaceType K) : (c * d).val v = c.val v * d.val v

@[simp]

theorem ArakelovDivisor.inv_val {K : Type u_1} [Field K] {hG : IsGlobalField K} (c : ArakelovDivisor K hG) (v : IsGlobalField.PlaceType K) : c⁻¹.val v = (c.val v)⁻¹

theorem ArakelovDivisor.ext {K : Type u_1} [Field K] {hG : IsGlobalField K} {c d : ArakelovDivisor K hG} (h : ∀ (v : IsGlobalField.PlaceType K), c.val v = d.val v) : c = d

theorem ArakelovDivisor.ext_iff {K : Type u_1} [Field K] {hG : IsGlobalField K} {c d : ArakelovDivisor K hG} : c = d ↔ ∀ (v : IsGlobalField.PlaceType K), c.val v = d.val v

@[implicit_reducible]

noncomputable instance ArakelovDivisor.instCommGroup {K : Type u_1} [Field K] {hG : IsGlobalField K} : CommGroup (ArakelovDivisor K hG)

def ArakelovDivisor.principal {K : Type u_1} [Field K] {hG : IsGlobalField K} (x : K) (hx : x ≠ 0) : ArakelovDivisor K hG

theorem ArakelovDivisor.hasFiniteMulSupport {K : Type u_1} [Field K] {hG : IsGlobalField K} (c : ArakelovDivisor K hG) : (Function.mulSupport c.val).Finite

noncomputable def ArakelovDivisor.size {K : Type u_1} [Field K] {hG : IsGlobalField K} (c : ArakelovDivisor K hG) : ℝ

@[simp]

theorem ArakelovDivisor.size_one {K : Type u_1} [Field K] {hG : IsGlobalField K} : size 1 = 1

theorem ArakelovDivisor.size_mul {K : Type u_1} [Field K] {hG : IsGlobalField K} (c d : ArakelovDivisor K hG) : (c * d).size = c.size * d.size

noncomputable def ArakelovDivisor.sizeHom {K : Type u_1} [Field K] {hG : IsGlobalField K} : ArakelovDivisor K hG →* ℝ

@[simp]

theorem ArakelovDivisor.sizeHom_apply {K : Type u_1} [Field K] {hG : IsGlobalField K} (c : ArakelovDivisor K hG) : sizeHom c = c.size

def ArakelovDivisor.L {K : Type u_1} [Field K] {hG : IsGlobalField K} (c : ArakelovDivisor K hG) : Set K