Theorems · Theorem · number theory

padicValNat.mul

∀ {p a b : ℕ} [hp : Fact (Nat.Prime p)], a ≠ 0 → b ≠ 0 → padicValNat p (a * b) = padicValNat p a + padicValNat p b

A rewrite lemma for padicValNat p (a * b) with conditions a ≠ 0, b ≠ 0.

Defined in

Mathlib.NumberTheory.Padics.PadicVal.Basic

Cited by

6 results in Mathlib

Foundations

Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Fact