FLT/NumberField/Completion/Finite.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. example (example at line 30) line 30 source
2. instance NumberField.instFiniteResidueFieldAdicCompletionIntegers line 39 source

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

   Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Finite, IsLocalRing.ResidueField, Subtype, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers

   Proof uses: Iff.mp, HasQuotient.Quotient, Ideal, IsDedekindDomain.HeightOneSpectrum.asIdeal, Equiv.finite_iff, RingEquiv.toEquiv, IsDedekindDomain.HeightOneSpectrum.ResidueFieldEquivCompletionResidueField, Ideal.finiteQuotientOfFreeOfNeBot, IsDedekindDomain.HeightOneSpectrum.ne_bot

   34 instances, coercions and auxiliary constants left out.

   Tactic trace: 2 steps

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

3. instance (instance at line 45) line 45 source
4. instance NumberField.instCompactSpaceAdicCompletionIntegers line 48 source

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

   Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, CompactSpace, Subtype, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers

   Proof uses: Valued.WithZeroMulInt.integer_compactSpace, inferInstance, Finite, Valued.ResidueField, WithZero, Multiplicative, Int, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_surjective

   21 instances, coercions and auxiliary constants left out.

5. lemma NumberField.isCompact_adicCompletionIntegers line 53 source

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

   Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, IsCompact, IsDedekindDomain.HeightOneSpectrum.adicCompletion, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers

   Proof uses: Eq.mpr, CompactSpace, Membership.mem, Set, id, Eq, congrArg, propext, isCompact_iff_compactSpace

   22 instances, coercions and auxiliary constants left out.

   Tactic trace: 2 steps

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

6. lemma NumberField.isOpenAdicCompletionIntegers line 58 source

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

   Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, IsOpen, IsDedekindDomain.HeightOneSpectrum.adicCompletion, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers

   Proof uses: Valued.isOpen_valuationSubring, WithZero, Multiplicative, Int

   16 instances, coercions and auxiliary constants left out.

7. instance Rat.adicCompletion.locallyCompactSpace line 62 source

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

   Statement uses: IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Rat, LocallyCompactSpace, IsDedekindDomain.HeightOneSpectrum.adicCompletion

   Proof uses: Topology.IsClosedEmbedding.locallyCompactSpace, Padic, Nat, Nat.Prime, Equiv, Nat.Primes, Rat.HeightOneSpectrum.primesEquiv, instFactPrimeValNat, Homeomorph, ContinuousAlgEquiv.toHomeomorph, Rat.HeightOneSpectrum.adicCompletion.padicEquiv, Homeomorph.isClosedEmbedding

   41 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

8. instance (instance at line 67) line 67 source
9. instance (instance at line 75) line 75 source
10. example (example at line 79) line 79 source

    Source comment

    does this exist upstream? Should do.

    example (v : HeightOneSpectrum (𝓞 K)) : SecondCountableTopology (v.adicCompletion K) :=
    …