leanprover-community/mathlib

Pull Requests Commits

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

stuart-presnell committed 3 years ago

d8b42674

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

chore(linear_algebra/*): Eliminate `finish` (#11074)

stuart-presnell committed 3 years ago

143fec64

feat(topology): missing lemmas for Kyle (#11076)

PatrickMassot committed 3 years ago

d053d57a

doc(combinatorics/configuration): Make comments into docstrings (#11097)

tb65536 committed 3 years ago

10771d7e

feat(data/polynomial/coeff): generalize to coeff_X_add_C_pow (#11093)

pechersky committed 3 years ago

d3aa0a43

chore(data/polynomial/eval): golf a proof, add versions (#11092)

urkud committed 3 years ago

afff1bbc

feat(measure_theory/integral/{interval,circle}_integral): add strict inequalities (#11061)

urkud committed 3 years ago

c04a42fe

feat(data/pi): bit[01]_apply simp lemmas (#11086)

pechersky committed 3 years ago

f452b383

feat(tactic/fin_cases): document `fin_cases with` and add `fin_cases using` (#11085)

robertylewis committed 3 years ago

94bb4667

feat(ring_theory/power_series/basic): add api for coeffs of shifts (#11082)

alexjbest committed 3 years ago

44f22aac

feat(data/set/finite): finite_or_infinite (#11084)

kmill committed 3 years ago

f0ca4338

feat(ring_theory/polynomial/cyclotomic/basic): add cyclotomic_expand_eq_cyclotomic (#10974)

riccardobrasca committed 3 years ago

612a4766

feat(ring_theory/polynomial/cyclotomic/basic): cyclotomic_prime_mul_X_sub_one (#11063)

ericrbg committed 3 years ago

10ea8609

feat(algebra/group_with_zero/power): With zero lemmas (#11051)

YaelDillies committed 3 years ago

294e78e7

fix(tactic/rcases): more with_desc fail (#11004)

digama0 committed 3 years ago

1332fe1a

feat(algebra/big_operators/order): `prod_eq_prod_iff_of_le` (#11068)

tb65536 committed 3 years ago

0e8cca36

refactor(combinatorics/configuration): Generalize results (#11065)

tb65536 committed 3 years ago

6ed17fc7

chore(order/*): Eliminate `finish` (#11064)

stuart-presnell committed 3 years ago

e1133ccc

split(data/list/infix): Split off `data.list.basic` (#11062)

YaelDillies committed 3 years ago

46566c5b

feat(algebra/group/units): generalize `units.coe_lift` (#11057)

urkud committed 3 years ago

2ecf4800

chore(ring_theory/unique_factorization_domain): Eliminate `finish` (#11055)

stuart-presnell committed 3 years ago

de6f57d2

feat(combinatorics/simple_graph/basic): edge deletion (#11054)

kmill committed 3 years ago

d67c4697

Newer Older