Def Ordnode.image

Modification history

2025-03-17 06:31

Mathlib/Data/Ordmap/Ordnode.lean

chore: Migrate to `DecidableLT` and `DecidableLE` (#22238) …

Modified Ordnode.image View on Github →

2024-12-11 04:11

Mathlib/Data/Ordmap/Ordnode.lean

chore: used named arguments instead of @DecidableRel (#19850)

Modified Ordnode.image View on Github →

2023-05-01 11:02

Mathlib/Data/Ordmap/Ordnode.lean

feat: port Mathlib.Data.Ordmap.Ordnode (#1455)

Added Ordnode.image View on Github →