leanprover-community/mathlib

Pull Requests Commits

Eliminate `finish` from `to_NFA_correct`

stuart-presnell committed 4 years ago

0c1f843d

Eliminate `finish` from `to_NFA_eval_from_match`

stuart-presnell committed 4 years ago

a41efd85

stuart-presnell committed 4 years ago

Verified 764e672a

Eliminate `finish` from `to_DFA_correct`

stuart-presnell committed 4 years ago

2e4ba669

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

stuart-presnell committed 4 years ago

143fec64

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

PatrickMassot committed 4 years ago

d053d57a

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

tb65536 committed 4 years ago

10771d7e

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

pechersky committed 4 years ago

d3aa0a43

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

urkud committed 4 years ago

afff1bbc

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

urkud committed 4 years ago

c04a42fe

Eliminate `finish` from `insert`

stuart-presnell committed 4 years ago

681343f2

Eliminate `finish` from `semilattice_inf.le_inf`

stuart-presnell committed 4 years ago

b9375009

Eliminate `finish` from `semilattice_inf.inv`

stuart-presnell committed 4 years ago

3187c8da

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

pechersky committed 4 years ago

f452b383

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

robertylewis committed 4 years ago

94bb4667

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

alexjbest committed 4 years ago

44f22aac

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

kmill committed 4 years ago

f0ca4338

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

riccardobrasca committed 4 years ago

612a4766

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

ericrbg committed 4 years ago

10ea8609

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

YaelDillies committed 4 years ago

294e78e7

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

digama0 committed 4 years ago

1332fe1a

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

tb65536 committed 4 years ago

0e8cca36

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

tb65536 committed 4 years ago

6ed17fc7

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

stuart-presnell committed 4 years ago

e1133ccc

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

YaelDillies committed 4 years ago

46566c5b

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

urkud committed 4 years ago

2ecf4800

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

stuart-presnell committed 4 years ago

de6f57d2

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

kmill committed 4 years ago

d67c4697

split(data/finsupp/order): Split off `data.finsupp.basic` (#11045)

YaelDillies committed 4 years ago

ca2c3443

feat(algebra/group_with_zero): add zero_mul_eq_const and mul_zero_eq_const (#11021)

eric-wieser committed 4 years ago

463be884

Newer Older