Theorem trans_trichotomous_right
Modification history
2026-02-06 11:53
Mathlib/Order/Defs/Unbundled.lean
chore(Order/Defs/Unbundled): deprecate `IsTrichotomous` in favor of core's `Std.Trichotomous` (#34349)
Modified trans_trichotomous_rightView on Github →2025-02-18 09:18
Mathlib/Order/Defs/Unbundled.lean
chore: move some results from Order.RelClasses earlier (#21144)
Modified trans_trichotomous_rightView on Github →