Theorem Rat.MulRingNorm.exists_minimal_nat_zero_lt_mulRingNorm_lt_one

Modification history

2025-01-02 20:35

Mathlib/NumberTheory/Ostrowski.lean

refactor(NumberTheory/Ostrowski): use `AbsoluteValue` instead of `MulRingNorm` (#20362) …

Deleted Rat.MulRingNorm.exists_minimal_nat_zero_lt_mulRingNorm_lt_one View on Github →

2024-06-25 09:57

Mathlib/NumberTheory/Ostrowski.lean

Feat (NumberTheory/Ostrowski): Proof of the non-archimedean case of Ostrowski's Theorem (#14026) …

Added Rat.MulRingNorm.exists_minimal_nat_zero_lt_mulRingNorm_lt_one View on Github →