leanprover-community/mathlib3

Pull Requests Commits

chore(data/hash_map): linting (#4498)

kmill committed 5 years ago

93790507

fix(algebra/ordered_group): use `add_neg` in autogenerated lemma name (#4580)

urkud committed 5 years ago

266895fb

feat(algebra/*_power): simplify `(-a)^(bit0 _)` and `(-a)^(bit1 _)` (#4573)

urkud committed 5 years ago

b3ce8837

feat(archive/imo): IMO 2020 Q2 (#4565)

jsm28 committed 5 years ago

38e9ed32

feat(algebra/free_algebra): Add an inductive principle (#4335)

eric-wieser committed 5 years ago

5022425a

feat(analysis/normed_space/multilinear): define `mk_pi_algebra` (#4316)

urkud committed 5 years ago

3d1f16aa

refactor(field_theory): Adjoin intermediate field (#4468)

tb65536 committed 5 years ago

1362701b

feat(data/polynomial/degree/erase_lead): definition and basic lemmas (#4527)

adomani committed 5 years ago

8fa91251

feat(ring_theory/witt_vector/structure_polynomial): witt_structure_int_prop (#4466)

jcommelin committed 5 years ago

0bfc68fc

feat(set_theory/cardinal): cardinality of powerset (#4576)

b-mehta committed 5 years ago

b9537177

chore(scripts): update nolints.txt (#4575)

leanprover-community-bot committed 5 years ago

81b8123d

chore(topology/algebra/group): review (#4570)

urkud committed 5 years ago

665cc13c

feat(data/nat/digits): add norm_digits tactic (#4452)

digama0 committed 5 years ago

952a407c

feat(analysis/calculus/times_cont_diff, analysis/calculus/inverse): smooth inverse function theorem (#4407)

hrmacbeth committed 5 years ago

b1ca33e0

feat(analysis/normed_space/inner_product): Cauchy-Schwarz equality case and other lemmas (#4571)

dupuisf committed 5 years ago

b48b4ff0

chore(linear_algebra/finite_dimensional): rename `of_finite_basis` (#4562)

urkud committed 5 years ago

0f085b98

chore(*): assorted lemmas (#4566)

urkud committed 5 years ago

14dcfe0c

chore(data/finsupp): replace `eq_zero_of_zero_eq_one` with `finsupp.unique_of_right` (#4563)

urkud committed 5 years ago

918e5d82

chore(measure_theory/measurable_space): add `finset.is_measurable_bUnion` etc (#4553)

urkud committed 5 years ago

33f7870a

chore(algebra/monoid_algebra): Reorder lemmas, name some sections for clarity (#4535)

eric-wieser committed 5 years ago

99130d84

chore(algebra/algebra/basic): fix definition of `ring_hom.to_algebra` (#4561)

urkud committed 5 years ago

0487a1d2

chore(order/well_founded): move to a file (#4568)

urkud committed 5 years ago

2c53e5ee

chore(scripts): update nolints.txt (#4564)

leanprover-community-bot committed 5 years ago

4dbebe3b

feat(data/finset/basic): equivalence of finsets from equivalence of types (#4560)

b-mehta committed 5 years ago

d8d6e18c

chore(topology/*): golf some proofs (#4528)

urkud committed 5 years ago

df5adc5c

feat(data/equiv/basic): equivalence on functions from bool (#4559)

b-mehta committed 5 years ago

c726898e

feat(data/finset/pi): pi singleton lemmas (#4558)

b-mehta committed 5 years ago

f91e0c68

feat(topology/uniform_space/cauchy): generalize `second_countable_of_separable` to uniform spaces (#4530)

urkud committed 5 years ago

c8738cb6

feat(analysis/special_functions/*): a few more simp lemmas (#4550)

urkud committed 5 years ago

6676917e

chore(scripts): update nolints.txt (#4556)

leanprover-community-bot committed 5 years ago

b084a068

Older