Mathlib Changelog
v4
Changelog
About
Github
Theorem
Rat.MulRingNorm.eq_on_Nat_iff_eq_on_Int
Modification history
2024-06-25 09:57
Mathlib/NumberTheory/Ostrowski.lean
Feat (NumberTheory/Ostrowski): Proof of the non-archimedean case of Ostrowski's Theorem (#14026) …
Deleted
Rat.MulRingNorm.eq_on_Nat_iff_eq_on_Int
View on Github →
2024-06-12 07:57
Mathlib/NumberTheory/Ostrowski.lean
Feat (Analysis/Normed/Ring/Seminorm): add lemmas on equivalence of MulRingNorms (#12517) …
Added
Rat.MulRingNorm.eq_on_Nat_iff_eq_on_Int
View on Github →