Embeddings

📁 Source: Mathlib/NumberTheory/NumberField/Cyclotomic/Embeddings.lean

Statistics

Metric	Count
Definitions	0
Theorems isTotallyComplex, nrComplexPlaces_eq_totient_div_two, nrRealPlaces_eq_zero	3
Total	3

IsCyclotomicExtension.Rat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isTotallyComplex 📖	mathematical	—	NumberField.IsTotallyComplex	—	IsCyclotomicExtension.numberField Rat.numberField Finite.of_fintype NumberField.nrRealPlaces_eq_zero_iff nrRealPlaces_eq_zero
nrComplexPlaces_eq_totient_div_two 📖	mathematical	—	NumberField.InfinitePlace.nrComplexPlaces IsCyclotomicExtension.numberField Set Set.instSingletonSet Rat.instField DivisionRing.toRatAlgebra Field.toDivisionRing Rat.numberField Finite.of_fintype Set.Elem Set.fintypeSingleton Nat.totient	—	IsCyclotomicExtension.numberField Rat.numberField Finite.of_fintype Nat.totient_even NumberField.to_charZero NumberField.InfinitePlace.card_add_two_mul_card_eq_rank Nat.instCharZero Nat.instAtLeastTwoHAddOfNat two_mul IsCyclotomicExtension.finrank instIsDomain Polynomial.cyclotomic.irreducible_rat NeZero.pos Nat.instCanonicallyOrderedAdd zero_add nrRealPlaces_eq_zero mul_div_cancel_left₀ Nat.instMulDivCancelClass eq_of_le_of_not_lt Nat.totient_two not_lt Nat.totient_one NumberField.InfinitePlace.nrComplexPlaces_eq_zero_of_finrank_eq_one
nrRealPlaces_eq_zero 📖	mathematical	—	NumberField.InfinitePlace.nrRealPlaces IsCyclotomicExtension.numberField Set Set.instSingletonSet Rat.instField DivisionRing.toRatAlgebra Field.toDivisionRing Rat.numberField Finite.of_fintype Set.Elem Set.fintypeSingleton	—	IsCyclotomicExtension.numberField Rat.numberField Finite.of_fintype NumberField.InfinitePlace.IsPrimitiveRoot.nrRealPlaces_eq_zero_of_two_lt IsCyclotomicExtension.zeta_spec

---

← Back to Index