Theorem PadicSeq.norm_mul

Modification history

2024-07-31 19:18
Mathlib/NumberTheory/Padics/PadicNumbers.lean
Chore: Remove some uses of `open Classical` (#15371) …
Modified PadicSeq.norm_mulView on Github →
2023-05-22 00:38
Mathlib/NumberTheory/Padics/PadicNumbers.lean
feat: port NumberTheory.Padics.PadicNumbers (#3095)
Added PadicSeq.norm_mulView on Github →