Def Nat.Primes.prodNatEquiv

Modification history

2024-11-21 17:01

Mathlib/Data/Nat/Factorization/PrimePow.lean

feat(Data/Nat/Factorization/PrimePow): add equivalence Primes × ℕ ≃ PrimePowers (#19335) …

Added Nat.Primes.prodNatEquiv View on Github →