Mathlib v3 is deprecated. Go to Mathlib v4

Theorem relation.refl_trans_gen_of_transitive_reflexive

Modification history

2020-06-02 00:43

src/logic/relation.lean

chore(*): split long lines (#2913)

Modified relation.refl_trans_gen_of_transitive_reflexive View on Github →

2018-04-26 18:29

logic/relation.lean

refactor(logic/relation,group_theory/free_group): add theory for reflextive/transitive relations & use them for the free group reduction

Added relation.refl_trans_gen_of_transitive_reflexive View on Github →