Theorems · Theorem · number theory
Rat.IsIntegralClosure.intEquiv_apply_eq_ringOfIntegersEquiv
∀ (x : NumberField.RingOfIntegers ℚ), (Rat.IsIntegralClosure.intEquiv (NumberField.RingOfIntegers ℚ)) x = Rat.ringOfIntegersEquiv x
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 158 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites19
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Algebra.algebraMapproof · cited by 4,706
- RingEquivstatement · cited by 1,147
- AlgEquiv.symmproof · cited by 615
- RingEquiv.symmproof · cited by 567
- NumberField.RingOfIntegersstatement and proof · cited by 413
- AlgEquiv.toRingEquivproof · cited by 137
- RingEquiv.transproof · cited by 54
- OneHom.mk.congr_simpproof · cited by 21
- MonoidHom.mk.congr_simpproof · cited by 21
- Classical.choose_eqproof · cited by 15
- AlgEquiv.ofAlgHom_applyproof · cited by 13
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.