Lemmas

📁 Source: FLT/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean

Statistics

Metric	Count
Definitions toHeightOneSpectrumInt, toHeightOneSpectrumRingOfIntegersRat, heightOneSpectrum, heightOneSpectrum_comap	4
Theorems	0
Total	4

Nat.Prime

Definitions

Name	Category	Theorems
toHeightOneSpectrumInt 📖	CompOp	—
toHeightOneSpectrumRingOfIntegersRat 📖	CompOp	3 math math: GaloisRepresentation.IsHardlyRamified.isUnramified, GaloisRepresentation.IsHardlyRamified.isFlat, GaloisRepresentation.IsHardlyRamified.three_adic

RingEquiv

Definitions

Name	Category	Theorems
heightOneSpectrum 📖	CompOp	—
heightOneSpectrum_comap 📖	CompOp	—

---

← Back to Index