Theorem Rat.IsIntegralClosure.intEquiv_apply_eq_ringOfIntegersEquiv

Modification history

2025-12-23 19:14
Mathlib/NumberTheory/Padics/HeightOneSpectrum.lean
fix: definition of `Rat.IsIntegralClosure.intEquiv` (#33203) …
Added Rat.IsIntegralClosure.intEquiv_apply_eq_ringOfIntegersEquivView on Github →