Theorem Nat.Primes.coe_prodNatEquiv_apply

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.coe_prodNatEquiv_applyView on Github →