Def LE.ofSetLike

Modification history

2026-09-15 16:52

Mathlib/Data/SetLike/Basic.lean

refactor(Data/SetLike): generalise `IsConcreteLE` (#42666) …

Deleted LE.ofSetLike View on Github →

2026-02-01 18:45

Mathlib/Data/SetLike/Basic.lean

refactor: remove order instances from `SetLike` (#32984) …

Added LE.ofSetLike View on Github →