Theorem Rat.coe_ringOfIntegersEquiv

Modification history

2025-11-13 22:45

Mathlib/NumberTheory/NumberField/Basic.lean

feat: ringOfIntegersEquiv_symm_coe (#31300) …

Deleted Rat.coe_ringOfIntegersEquiv View on Github →

2025-01-08 18:30

Mathlib/NumberTheory/NumberField/Basic.lean

feat(NumberTheory/NumberField/Basic): ringOfIntegersEquiv API (#20544) …

Added Rat.coe_ringOfIntegersEquiv View on Github →