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 |
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...