Commit 2022-07-22 02:20 c97887bd

View on Github →

refactor(data/list/chain): transitive → is_trans on chain.pairwise (#15571) Apart from being more widely used throughout mathlib, is_trans can be inferred when used with common relations such as ≤, <, ∣, and others.

Estimated changes

Modified src/data/list/chain.lean

modified theorem list.chain'_iff_pairwise

modified theorem list.chain_iff_pairwise

Modified src/data/list/cycle.lean

modified theorem cycle.chain_iff_pairwise

modified theorem cycle.forall_eq_of_chain

Modified src/data/list/range.lean

Modified src/data/nat/prime.lean

Modified src/logic/equiv/list.lean