Revision 65a1391a0106c9204fe45bc73a039f056558cb83 authored by Yaël Dillies on 30 October 2023, 15:07:49 UTC, committed by Yaël Dillies on 30 October 2023, 15:07:49 UTC
Left commutativity and cardinality of `list.filter`/`multiset.filter`/`finset.filter`. Interaction of `count`/`countp` and `attach`.
1 parent 3365b20
| File | Mode | Size |
|---|---|---|
| canonically_ordered_comm_semiring_two_mul.lean | -rw-r--r-- | 8.9 KB |
| char_p_zero_ne_char_zero.lean | -rw-r--r-- | 1.1 KB |
| cyclotomic_105.lean | -rw-r--r-- | 3.8 KB |
| direct_sum_is_internal.lean | -rw-r--r-- | 3.7 KB |
| girard.lean | -rw-r--r-- | 2.3 KB |
| homogeneous_prime_not_prime.lean | -rw-r--r-- | 5.7 KB |
| leanpkg.toml | -rw-r--r-- | 110 bytes |
| linear_order_with_pos_mul_pos_eq_zero.lean | -rw-r--r-- | 2.3 KB |
| map_floor.lean | -rw-r--r-- | 4.7 KB |
| phillips.lean | -rw-r--r-- | 28.6 KB |
| pseudoelement.lean | -rw-r--r-- | 5.3 KB |
| quadratic_form.lean | -rw-r--r-- | 2.0 KB |
| seminorm_lattice_not_distrib.lean | -rw-r--r-- | 3.1 KB |
| sorgenfrey_line.lean | -rw-r--r-- | 14.1 KB |
| zero_divisors_in_add_monoid_algebras.lean | -rw-r--r-- | 11.2 KB |
Computing file changes ...
