Theorem transGen_of_succ_of_reflexive

Modification history

2026-04-14 12:34
Mathlib/Order/SuccPred/Relation.lean
chore(Order/Defs/Unbundled): deprecate `def Reflexive` in favor of `class Std.Refl` (#37278) …
Deleted transGen_of_succ_of_reflexiveView on Github →
2023-01-02 20:39
Mathlib/Order/SuccPred/Relation.lean
feat: port Order.SuccPred.Relation (#1295) …
Added transGen_of_succ_of_reflexiveView on Github →