FLT/Mathlib/NumberTheory/NumberField/AdeleRing.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Topological facts about adele rings

This should be enough to deduce that they're Polish.

Imports (3)
Imported by 4 files
  1. lemma NumberField.AdeleRing.add_fst line 29 source

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

    Statement uses: Field, CommRing, IsDedekindDomain, Algebra, IsFractionRing, NumberField.AdeleRing, Eq, NumberField.InfiniteAdeleRing, Prod.fst, IsDedekindDomain.FiniteAdeleRing, HAdd.hAdd

    Proof uses: rfl

    17 instances, coercions and auxiliary constants left out.

  2. lemma NumberField.AdeleRing.add_snd line 30 source

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

    Statement uses: Field, CommRing, IsDedekindDomain, Algebra, IsFractionRing, NumberField.AdeleRing, Eq, IsDedekindDomain.FiniteAdeleRing, Prod.snd, NumberField.InfiniteAdeleRing, HAdd.hAdd

    Proof uses: rfl

    17 instances, coercions and auxiliary constants left out.

  3. lemma NumberField.AdeleRing.mul_fst line 32 source

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

    Statement uses: Field, CommRing, IsDedekindDomain, Algebra, IsFractionRing, NumberField.AdeleRing, Eq, NumberField.InfiniteAdeleRing, Prod.fst, IsDedekindDomain.FiniteAdeleRing, HMul.hMul

    Proof uses: rfl

    17 instances, coercions and auxiliary constants left out.

  4. lemma NumberField.AdeleRing.mul_snd line 33 source

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

    Statement uses: Field, CommRing, IsDedekindDomain, Algebra, IsFractionRing, NumberField.AdeleRing, Eq, IsDedekindDomain.FiniteAdeleRing, Prod.snd, NumberField.InfiniteAdeleRing, HMul.hMul

    Proof uses: rfl

    17 instances, coercions and auxiliary constants left out.

  5. lemma NumberField.AdeleRing.zero_fst line 35 source

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

    Statement uses: Field, CommRing, IsDedekindDomain, Algebra, IsFractionRing, Eq, NumberField.InfiniteAdeleRing, Prod.fst, IsDedekindDomain.FiniteAdeleRing, OfNat.ofNat, NumberField.AdeleRing

    Proof uses: rfl

    17 instances, coercions and auxiliary constants left out.

  6. lemma NumberField.AdeleRing.zero_snd line 36 source

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

    Statement uses: Field, CommRing, IsDedekindDomain, Algebra, IsFractionRing, Eq, IsDedekindDomain.FiniteAdeleRing, Prod.snd, NumberField.InfiniteAdeleRing, OfNat.ofNat, NumberField.AdeleRing

    Proof uses: rfl

    17 instances, coercions and auxiliary constants left out.

  7. lemma NumberField.AdeleRing.one_fst line 38 source

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

    Statement uses: Field, CommRing, IsDedekindDomain, Algebra, IsFractionRing, Eq, NumberField.InfiniteAdeleRing, Prod.fst, IsDedekindDomain.FiniteAdeleRing, OfNat.ofNat, NumberField.AdeleRing

    Proof uses: rfl

    21 instances, coercions and auxiliary constants left out.

  8. lemma NumberField.AdeleRing.one_snd line 39 source

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

    Statement uses: Field, CommRing, IsDedekindDomain, Algebra, IsFractionRing, Eq, IsDedekindDomain.FiniteAdeleRing, Prod.snd, NumberField.InfiniteAdeleRing, OfNat.ofNat, NumberField.AdeleRing

    Proof uses: rfl

    21 instances, coercions and auxiliary constants left out.

  9. instance NumberField.AdeleRing.locallyCompactSpace line 46 source

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

    Statement uses: Field, NumberField, LocallyCompactSpace, NumberField.AdeleRing, NumberField.RingOfIntegers

    6 instances, coercions and auxiliary constants left out.

  10. instance NumberField.AdeleRing.(instance at line 49) line 49 source
  11. instance NumberField.AdeleRing.(instance at line 52) line 52 source