Theorem Rat.MulRingNorm.equiv_on_Nat_iff_equiv

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.equiv_on_Nat_iff_equivView 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.equiv_on_Nat_iff_equivView on Github →