Theorem Even.tsub
Modification history
2024-10-24 21:25
Mathlib/Algebra/Order/Sub/Basic.lean
feat: use aliases for `CovariantClass α α (· * ·) (· ≤ ·)` etc (#13154)
Modified Even.tsubView on Github →2024-08-17 12:07
Mathlib/Algebra/Order/Sub/Basic.lean
chore (Data.Multiset.Basic): avoid bundled ordered algebra for basic results on multisets (#14477) …
Modified Even.tsubView on Github →2024-07-31 23:15
Mathlib/Algebra/Order/Sub/Canonical.lean
chore: backports for leanprover/lean4#4814 (part 6) (#15313) …
Modified Even.tsubView on Github →2024-05-15 09:43
Mathlib/Algebra/Order/Sub/Canonical.lean
move(Algebra/Parity): Split file (#12829) …
Modified Even.tsubView on Github →