n : ℕ+
m : ℕ
u : PrimeMultiset := factorMultiset n
⊢ factorMultiset (Pow.pow n m) = m • factorMultiset n
n : ℕ+
m : ℕ
⊢ factorMultiset (Pow.pow n m) = m • factorMultiset n
let u := factorMultiset n
n : ℕ+
m : ℕ
u : PrimeMultiset := factorMultiset n
this : n = PrimeMultiset.prod u
⊢ factorMultiset (Pow.pow n m) = m • factorMultiset n
n : ℕ+
m : ℕ
u : PrimeMultiset := factorMultiset n
⊢ factorMultiset (Pow.pow n m) = m • factorMultiset n
have : n = u.prod := (prod_factorMultiset n).symm
n : ℕ+
m : ℕ
u : PrimeMultiset := factorMultiset n
this : n = PrimeMultiset.prod u
⊢ factorMultiset (PrimeMultiset.prod (m • u)) = m • factorMultiset (PrimeMultiset.prod u)
n : ℕ+
m : ℕ
u : PrimeMultiset := factorMultiset n
this : n = PrimeMultiset.prod u
⊢ factorMultiset (Pow.pow n m) = m • factorMultiset n
rw [this, ← PrimeMultiset.prod_smul]
no goals
n : ℕ+
m : ℕ
u : PrimeMultiset := factorMultiset n
this : n = PrimeMultiset.prod u
⊢ factorMultiset (PrimeMultiset.prod (m • u)) = m • factorMultiset (PrimeMultiset.prod u)
repeat' rw [PrimeMultiset.factorMultiset_prod]
no goals
n : ℕ+
m : ℕ
u : PrimeMultiset := factorMultiset n
this : n = PrimeMultiset.prod u
⊢ m • u = m • factorMultiset (PrimeMultiset.prod u)
rw [PrimeMultiset.factorMultiset_prod]