FLT/Mathlib/NumberTheory/NumberField/InfinitePlace/Completion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Completion

Material destined for Mathlib.

Imports (1)
Imported by 2 files
  1. instance NumberField.InfinitePlace.Completion.secondCountableTopology line 20 source

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

    Statement uses: Field, NumberField.InfinitePlace, SecondCountableTopology, NumberField.InfinitePlace.Completion

    Proof uses: Topology.IsInducing.secondCountableTopology, Complex, RingHom, NumberField.InfinitePlace.Completion.extensionEmbedding, Topology.IsEmbedding.isInducing, Isometry.isEmbedding, NumberField.InfinitePlace.Completion.isometry_extensionEmbedding

    32 instances, coercions and auxiliary constants left out.