case a
p : Nat.Primes
⊢ ↑factorMultisetEquiv.symm (factorMultiset ↑p) = ↑factorMultisetEquiv.symm (PrimeMultiset.ofPrime p)
p : Nat.Primes
⊢ factorMultiset ↑p = PrimeMultiset.ofPrime p
apply factorMultisetEquiv.symm.injective
case a
p : Nat.Primes
⊢ PrimeMultiset.prod (factorMultiset ↑p) = PrimeMultiset.prod (PrimeMultiset.ofPrime p)
case a
p : Nat.Primes
⊢ ↑factorMultisetEquiv.symm (factorMultiset ↑p) = ↑factorMultisetEquiv.symm (PrimeMultiset.ofPrime p)
change (p : ℕ+).factorMultiset.prod = (PrimeMultiset.ofPrime p).prod
no goals
case a
p : Nat.Primes
⊢ PrimeMultiset.prod (factorMultiset ↑p) = PrimeMultiset.prod (PrimeMultiset.ofPrime p)
rw [(p : ℕ+).prod_factorMultiset, PrimeMultiset.prod_ofPrime]