Commit 2023-01-25 21:06 090fcabe

View on Github →

Feat: prove IsTrans α r → Trans r r r and Trans r r r → IsTrans α r (#1522) Now Trans.trans conflicts with _root_.trans.

Estimated changes

Modified Mathlib/Algebra/Associated.lean

Modified Mathlib/Algebra/CovariantAndContravariant.lean

Modified Mathlib/Algebra/Divisibility/Basic.lean

Modified Mathlib/Algebra/Order/Monoid/Lemmas.lean

Modified Mathlib/Data/Fin/Basic.lean

Modified Mathlib/Data/Finset/Card.lean

Modified Mathlib/Data/Finset/Order.lean

Modified Mathlib/Data/Fintype/Card.lean

Modified Mathlib/Data/Int/ModEq.lean

Modified Mathlib/Data/List/Chain.lean

Modified Mathlib/Data/List/Forall2.lean

Modified Mathlib/Data/List/Sort.lean

Modified Mathlib/Data/Multiset/Basic.lean

Modified Mathlib/Data/Prod/Basic.lean

Modified Mathlib/Data/Sigma/Lex.lean

Modified Mathlib/Data/Sum/Order.lean

Modified Mathlib/Init/Algebra/Classes.lean

Modified Mathlib/Order/Chain.lean

Modified Mathlib/Order/Extension/Linear.lean

Modified Mathlib/Order/InitialSeg.lean

Modified Mathlib/Order/Monotone/Basic.lean

Modified Mathlib/Order/RelClasses.lean

modified theorem ssubset_trans

modified theorem subset_trans

modified theorem transitive_of_trans

Modified Mathlib/Order/WellFounded.lean