Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-11-13 22:45
8af997f0
View on Github →
feat: ringOfIntegersEquiv_symm_coe (
#31300
) This is upstreamed from the FLT project.
Estimated changes
Modified
Mathlib/NumberTheory/NumberField/Basic.lean
deleted
theorem
Rat.coe_ringOfIntegersEquiv
added
theorem
Rat.ringOfIntegersEquiv_apply_coe
added
theorem
Rat.ringOfIntegersEquiv_symm_apply_coe