leanprover-community/mathlib

Pull Requests Commits

Merge branch 'SP_count_map' into SP_perm_nodup

stuart-presnell committed 3 years ago

6b070a6b

Various junk experiments

stuart-presnell committed 3 years ago

ed81ce10

Rename `count_map_map` to `count_map_of_injective`

stuart-presnell committed 3 years ago

7c975874

stuart-presnell committed 3 years ago

ebb76dc5

Rename variables

stuart-presnell committed 3 years ago

965de579

Add lemma `count_le_count_map`

stuart-presnell committed 3 years ago

7f926cd8

feat(ring_theory/polynomial/cyclotomic/basic): add cyclotomic_expand_eq_cyclotomic_mul (#11005)

riccardobrasca committed 3 years ago

52841fbf

chore(topology/algebra/weak_dual_topology): review (#11141)

urkud committed 3 years ago

655c2f06

feat(analysis/inner_product_space/adjoint): define the adjoint for linear maps between finite-dimensional spaces (#11119)

dupuisf committed 3 years ago

04071ae3

feat(data/nat/prime): min fac of a power (#11115)

b-mehta committed 3 years ago

9443a7b3

feat(logic/small): The image of a small set is small (#11108)

vihdzp committed 3 years ago

0b6f9ebb

feat(combinatorics/simple_graph): lemmas describing edge set of subgraphs (#11087)

b-mehta committed 3 years ago

864a43bc

chore(data/nat/prime): move some results (#11066)

Ruben-VandeVelde committed 3 years ago

8f873b72

feat(analysis/special_functions/log): sum of logs is log of product (#11106)

b-mehta committed 3 years ago

0c149c90

chore(measure_theory/function/lp_space): move `fact`s (#11107)

hrmacbeth committed 3 years ago

23fdf99d

feat(topology/algebra): range of `coe_fn : (M₁ →ₛₗ[σ] M₂) → (M₁ → M₂)` is closed (#11105)

urkud committed 3 years ago

4f3e99a6

feat(analysis/normed_space/dual): add lemmas, golf (#11132)

urkud committed 3 years ago

ea95523d

feat(topology/metric_space/lipschitz): image of a bdd set (#11134)

urkud committed 3 years ago

be17b92a

chore(analysis/normed_space/basic): add `normed_space.unbounded_univ` (#11131)

urkud committed 3 years ago

5bfd9245

split(data/finsupp/multiset): Split off `data.finsupp.basic` (#11110)

YaelDillies committed 3 years ago

5ac87153

chore(data/*): Eliminate `finish` (#11099)

stuart-presnell committed 3 years ago

b8833e9e

feat(algebra/ne_zero): typeclass for n ≠ 0 (#11033)

ericrbg committed 3 years ago

2a929f24

chore(*): Eliminate some more instances of `finish` (#11136)

stuart-presnell committed 3 years ago

dd65894b

chore(number_theory/quadratic_reciprocity): Eliminate `finish` (#11133)

stuart-presnell committed 3 years ago

d67a1dc6

chore(algebra/continued_fractions/computation/translations): Eliminate `finish` (#11130)

stuart-presnell committed 3 years ago

c03dbd16

chore(computability/NFA): Eliminate `finish` (#11103)

stuart-presnell committed 3 years ago

90d12bb1

chore([normed/charted]_space): Eliminate `finish` (#11126)

stuart-presnell committed 3 years ago

6703cdda

feat(algebra/order/field): prove `a / a ≤ 1` (#11118)

urkud committed 3 years ago

c25bd03e

chore(topology/metric_space/basic): +1 version of Heine-Borel (#11127)

urkud committed 3 years ago

395e2755

feat(data/list/pairwise): pairwise repeat (#11117)

b-mehta committed 3 years ago

cb37df34

Older