Theorem Finsupp.isPWO

Modification history

2024-11-04 23:02

Mathlib/Data/Finsupp/PWO.lean

chore(*): `LinearOrder` + `IsWellOrder α (· < ·)` → `LinearOrder` + `WellFoundedLT` (#18217) …

Modified Finsupp.isPWO View on Github →

2024-01-09 15:48

Mathlib/Data/Finsupp/PWO.lean

chore(*): rename IsPwo to IsPWO (#9582) …

Added Finsupp.isPWO View on Github →