Theorem Rat.MulRingNorm.mulRingNorm_equiv_padic_of_bounded

Modification history

2025-01-02 20:35

Mathlib/NumberTheory/Ostrowski.lean

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

Deleted Rat.MulRingNorm.mulRingNorm_equiv_padic_of_bounded 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.mulRingNorm_equiv_padic_of_bounded View on Github →