Theorem PNat.coe_injective

Modification history

2024-11-28 15:29
Mathlib/Data/PNat/Defs.lean
feat: Define `Nat.finMulAntidiagonal`, the `Finset` of tuples of naturals with a fixed product. (#10668) …
Modified PNat.coe_injectiveView on Github →
2022-11-17 12:36
Mathlib/Data/PNat/Defs.lean
feat: port Data.PNat.Defs (#604) …
Added PNat.coe_injectiveView on Github →