Theorem rel_congr_left

Modification history

2025-02-18 09:18

Mathlib/Order/Defs/Unbundled.lean

chore: move some results from Order.RelClasses earlier (#21144)

Modified rel_congr_left View on Github →

2025-01-26 13:15

Mathlib/Order/RelClasses.lean

feat(Order/Antisymmetrization): `AntisymmRel` lemmas (#19571) …

Added rel_congr_left View on Github →