Theorems · Definition · number theory

IsDedekindDomain.selmerGroup

{R : Type u} →
  [inst : CommRing R] →
    [IsDedekindDomain R] →
      {K : Type v} →
        [inst_2 : Field K] →
          [inst_3 : Algebra R K] →
            [IsFractionRing R K] →
              {S : Set (IsDedekindDomain.HeightOneSpectrum R)} → {n : ℕ} → Subgroup (Kˣ ⧸ (powMonoidHom n).range)

The Selmer group K⟮S, n⟯.

Defined in

Mathlib.RingTheory.DedekindDomain.SelmerGroup

Cited by

4 results in Mathlib

Foundations

Depth 165 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIsDedekindDomainFieldAlgebraIsFractionRing