Theorem padicValNat_prime_prime_pow

Modification history

2026-11-01 22:20

Mathlib/NumberTheory/Padics/PadicVal/Basic.lean

refactor: replace `padicValNat` with `multiplicity` (#43722) …

Deleted padicValNat_prime_prime_pow View on Github →

2024-04-05 19:57

Mathlib/NumberTheory/Padics/PadicVal.lean

feat(NumberTheory/Padics/PadicVal): Add `padicValNat_mul_pow_left/right` (#11354) …

Added padicValNat_prime_prime_pow View on Github →