selmerGroup — Mathlib

English

The Selmer group K⟮S,n⟯ is the subgroup of K/n consisting of classes x whose valuation is 1 at all v outside S.

Русский

Группа Selmer K⟮S,n⟯ есть подгруппа K/n, состоящая из классов x, для которых оценка равна 1 во всех v вне S.

LaTeX

$$K⟮S,n⟯ = { x ∈ K/n : ∀ v ∉ S, v.valuationOfNeZeroMod n x = 1 }$$

Lean4

/-- The Selmer group `K⟮S, n⟯`. -/
def selmerGroup : Subgroup <| K / n
    where
  carrier := {x : K / n | ∀ (v) (_ : v ∉ S), (v : HeightOneSpectrum R).valuationOfNeZeroMod n x = 1}
  one_mem' _ _ := by rw [map_one]
  mul_mem' hx hy v hv := by rw [map_mul, hx v hv, hy v hv, one_mul]
  inv_mem' hx v
    hv := by
    rw [map_inv, hx v hv, inv_one]
      -- Porting note: was `scoped[SelmerGroup]` but that does not work even using `open SelmerGroup`

Похожие утверждения