FLT/Mathlib/NumberTheory/NumberField/FiniteAdeleRing.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Finite Adele Ring

Material destined for Mathlib.

Imports (8)
Imported by 8 files
  1. instance IsDedekindDomain.FiniteAdeleRing.(instance at line 50) line 50 source
  2. instance IsDedekindDomain.FiniteAdeleRing.(instance at line 56) line 56 source
  3. lemma IsDedekindDomain.FiniteAdeleRing.isCompact_integralAdeles line 60 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Field, NumberField, IsCompact, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Subring, IsDedekindDomain.FiniteAdeleRing.integralAdeles

    Proof uses: Iff.mpr, CompactSpace, Membership.mem, Set, isCompact_iff_compactSpace

    24 instances, coercions and auxiliary constants left out.

  4. instance IsDedekindDomain.FiniteAdeleRing.(instance at line 63) line 63 source
  5. instance IsDedekindDomain.FiniteAdeleRing.(instance at line 66) line 66 source
  6. lemma IsDedekindDomain.FiniteAdeleRing.HeightOneSpectrum.nonempty line 69 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: CommRing, Not, IsField, Nontrivial, Nonempty, IsDedekindDomain.HeightOneSpectrum

    Proof uses: Ideal, Ideal.IsMaximal, Exists, Ideal.exists_maximal, Nonempty.intro, IsDedekindDomain.HeightOneSpectrum.mk, inferInstance, Ideal.IsPrime, Eq, Bot.bot, False, Iff.mpr, Ring.isField_iff_maximal_bot, Eq.symm

    10 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

    Open to load the checked before-and-after goal states.

  7. instance IsDedekindDomain.FiniteAdeleRing.(instance at line 74) line 74 source
  8. instance IsDedekindDomain.FiniteAdeleRing.(instance at line 81) line 81 source