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

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Basic

Material destined for Mathlib.

Imports (1)
Imported by 2 files
  1. lemma Rat.infinitePlace_isReal line 23 source

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

    Statement uses: NumberField.InfinitePlace, Rat, NumberField.InfinitePlace.IsReal

    Proof uses: Eq.rec, Rat.infinitePlace, Eq, Rat.isReal_infinitePlace, Eq.symm, Subsingleton.elim

    3 instances, coercions and auxiliary constants left out.