leanprover-community/mathlib

Pull Requests Commits

Merge branch 'SP_misc_finish' into SP_finish_double_check

stuart-presnell committed 3 years ago

c89c073f

Merge branch 'SP_quadratic_finish' into SP_finish_double_check

stuart-presnell committed 3 years ago

d68aecc5

Merge branch 'SP_CF_finish' into SP_finish_double_check

stuart-presnell committed 3 years ago

e4847c73

Merge branch 'SP_manifold_finish' into SP_finish_double_check

stuart-presnell committed 3 years ago

c69395d8

Merge branch 'SP_NFA_finish' into SP_finish_double_check

stuart-presnell committed 3 years ago

ec35c327

Merge branch 'SP_data_finish' into SP_finish_double_check

stuart-presnell committed 3 years ago

dae9251e

Eliminate `finish` from `not_first_wins`

stuart-presnell committed 3 years ago

e6edd019

Eliminate `finish` from `Mon_to_Monad`

stuart-presnell committed 3 years ago

07836c9b

Eliminate `finish` from `mod_swap`

stuart-presnell committed 3 years ago

e76df598

Eliminate `finish` from `legendre_sym_two`

stuart-presnell committed 3 years ago

37ee2da9

Eliminate `finish` from `legendre_sym_eq_one_iff`

stuart-presnell committed 3 years ago

e5548bc2

Eliminate `finish` from `sum_Ico_eq_card_lt`

stuart-presnell committed 3 years ago

3fc9c331

stuart-presnell committed 3 years ago

2ed99b1b

Eliminate `finish` from `exists_succ_nth_stream_of_fr_zero`

stuart-presnell committed 3 years ago

8fd37661

Eliminate `finish` from `succ_nth_stream_eq_some_iff`

stuart-presnell committed 3 years ago

2280e13c

Eliminate `finish` from `succ_nth_stream_eq_none_iff`

stuart-presnell committed 3 years ago

3767c640

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

chore(algebra/big_operators/finprod): Eliminate `finish` (#10923)

stuart-presnell committed 3 years ago

d8b42674

Eliminate `finish` from `normed_lattice_add_comm_group`

stuart-presnell committed 3 years ago

a1107a4e

`finish` from `exists_subset_affine_independent_span_eq_top_of_open`

stuart-presnell committed 3 years ago

6a0801a6

Eliminate `finish` from `id_groupoid`

stuart-presnell committed 3 years ago

e2be3560

feat(data/polynomial): more API for roots (#11081)

pechersky committed 3 years ago

e003d6e2

chore(topology/metric_space/basic): golf, add dot notation (#11111)

urkud committed 3 years ago

268d1a86

feat(data/polynomial/basic): `add_submonoid.closure` of monomials is `⊤` (#11101)

urkud committed 3 years ago

a82c4819

feat(data/option/basic): add `eq_of_mem_of_mem` (#11098)

stuart-presnell committed 3 years ago

134ff7d2

feat(analysis/special_functions/pow): `rpow` as an `order_iso` (#10831)

j-loreaux committed 3 years ago

f11d3ca2

feat(logic/small): The range of a function from a small type is small (#11029)

vihdzp committed 3 years ago

8d41552f

refactor(category_theory/shift): make shifts more flexible (#10573)

jcommelin committed 3 years ago

8d24a1fe

chore(ring_theory/*): Eliminate `finish` (#11100)

stuart-presnell committed 3 years ago

0b80d0cb

Older