Kim Morrison a62dabeb56 feat: nodup_keys theorems for maps (#10159) ... This PR adds `nodup_keys` lemmas as corollaries of existing `distinct_keys` to all `Map` variants.		2025-08-28 06:00:28 +00:00
..
Classes.lean	feat: package factories for order typeclasses (#9797)	2025-08-19 13:43:29 +00:00
ClassesExtra.lean	feat: package factories for order typeclasses based on Ord (#9916)	2025-08-20 11:14:07 +00:00
Factories.lean	feat: improvements to Min/Max-related classes (#10024)	2025-08-22 07:08:00 +00:00
FactoriesExtra.lean	feat: package factories for order typeclasses based on Ord (#9916)	2025-08-20 11:14:07 +00:00
Lemmas.lean	feat: more convenient creation of polymorphic range instances (#10005)	2025-08-22 07:08:33 +00:00
LemmasExtra.lean	feat: package factories for order typeclasses based on Ord (#9916)	2025-08-20 11:14:07 +00:00
Ord.lean	feat: nodup_keys theorems for maps (#10159)	2025-08-28 06:00:28 +00:00
PackageFactories.lean	chore: fix spelling errors (#10042)	2025-08-22 07:23:12 +00:00