Theorems · Definition · number theory
Rat.IsIntegralClosure.intEquiv
(R : Type u_1) → [inst : CommRing R] → [inst_1 : Algebra R ℚ] → [IsIntegralClosure R ℤ ℚ] → R ≃+* ℤ
If R has field of fractions ℚ and is the integral closure of ℤ in ℚ then it is
isomorphic to ℤ.
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 152 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- Algebrastatement and proof · cited by 11,388
- RingEquivstatement · cited by 1,147
- RingEquiv.symmproof · cited by 567
- IsIntegralClosurestatement and proof · cited by 146
- RingEquiv.transproof · cited by 54
- Rat.ringOfIntegersEquivproof · cited by 6
- NumberField.RingOfIntegers.equivproof · cited by 0
Cited by8
Results whose statement or proof uses this declaration.
- Rat.HeightOneSpectrum.primesEquivproof · cited by 6
- Rat.HeightOneSpectrum.natGeneratorproof · cited by 5
- Rat.HeightOneSpectrum.prime_natGeneratorproof · cited by 1
- Rat.HeightOneSpectrum.span_natGeneratorstatement and proof · cited by 1
- Rat.IsIntegralClosure.intEquiv.congr_simpstatement and proof · cited by 0
- Rat.HeightOneSpectrum.natGenerator_dvd_iffstatement · cited by 0
- Rat.HeightOneSpectrum.valuation_equiv_padicValuationproof · cited by 0
- Rat.IsIntegralClosure.intEquiv_apply_eq_ringOfIntegersEquivstatement · cited by 0