Theorem padicValNat.maxPowDiv_eq_multiplicity_get

Modification history

2024-10-16 04:43

Mathlib/NumberTheory/Padics/PadicVal/Basic.lean

refactor(RingTheory/Multiplicity): split to Nat-valued `multiplicity` and ENat-valued `emultiplicity` (#16881) …

Deleted padicValNat.maxPowDiv_eq_multiplicity_get View on Github →

2023-06-18 08:20

Mathlib/NumberTheory/Padics/PadicVal.lean

feat: add Nat.maxPowDiv (#5158) …

Added padicValNat.maxPowDiv_eq_multiplicity_get View on Github →