leanprover-community/mathlib

Pull Requests Commits

laughinggas committed 4 years ago

39e5c125

moved everything

laughinggas committed 4 years ago

8b44b23c

feat(algebra/ordered_ring): weaken hypotheses for one_le_two (#6034)

b-mehta committed 4 years ago

6df15017

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

leanprover-community-bot committed 4 years ago

3309490a

feat(data/list/basic): drop_eq_nil_of_le (#6029)

pechersky committed 4 years ago

7812afa3

feat(order/(complete_lattice, compactly_generated)): independent sets in a complete lattice (#5971)

awainverse committed 4 years ago

cbd67cf4

feat(linear_algebra/free_algebra): Show that free_monoid forms a basis over free_algebra (#5868)

eric-wieser committed 4 years ago

5f328b6e

feat(data/nat/factorial): additional inequalities (#6026)

adomani committed 4 years ago

36b35107

feat(data/real/sqrt): added some missing sqrt lemmas (#5933)

benjamindavidson committed 4 years ago

360fa07e

chore(analysis/calculus): rename `has_f?deriv_at_unique` to `has_f?deriv_at.unique` (#6019)

urkud committed 4 years ago

bb15b1ce

doc(lint/simp): typesetting issues in simp_nf library note (#6018)

robertylewis committed 4 years ago

235a7c46

chore(data/nat/parity): rename type variable (#6016)

benjamindavidson committed 4 years ago

9a0d2b23

feat(algebra/polynomial/big_operators): add degree_prod lemma (#5979)

BoltonBailey committed 4 years ago

fa8df59b

feat(linear_algebra/sesquilinear_form): add composition between sesquilinear forms and linear maps (#5729)

kex-y committed 4 years ago

5a9ca8d3

doc(algebra/{archimedean, char_zero}): provide docstrings (#6010)

Julian-Kuelshammer committed 4 years ago

e1ca806c

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

leanprover-community-bot committed 4 years ago

e66ad5f5

feat(order/compactly_generated): Show that the sublattice below a compact element is coatomic (#5942)

cemulate committed 4 years ago

79ca6e23

feat(algebra/ring): add mk_mul_self_of_two_ne_zero (#5862)

alexjbest committed 4 years ago

fcad25f2

feat(data/fintype/sort): add `fin_sum_equiv_of_finset` (#6008)

urkud committed 4 years ago

2153dc34

refactor(measure_theory/*): rename `is_(null_)?measurable` to `(null_)?measurable_set` (#6001)

urkud committed 4 years ago

1b1ad15c

chore(analysis/normed_space/basic): use explicit arg `𝕜'` in lemmas about `normed_algebra` (#6009)

urkud committed 4 years ago

2b2edc97

fix(tactic/delta_instance): improve naming of instances with multiple arguments (#6007)

eric-wieser committed 4 years ago

4e786548

feat(geometry/manifold/instances): sphere is a smooth manifold (#5607)

hrmacbeth committed 4 years ago

fe9c021d

refactor(group_theory/perm): move perm.subtype_perm to basic (#6005)

pechersky committed 4 years ago

dbb5ca1e

feat(nat/basic): more nat.find lemmas (#6002)

fpvandoorn committed 4 years ago

9b3dc417

feat(analysis/normed_space/inner_product): remove unnecessary `nonneg_im` field (#5999)

gebner committed 4 years ago

6633a70e

feat(logic/function/basic): add bijective.iff_exists_unique and projections (#5995)

eric-wieser committed 4 years ago

508c2650

refactor(data/polynomial/eval): change eval_smul lemmas to use * instead of 2nd smul (#5991)

BoltonBailey committed 4 years ago

3732fb9d

feat(algebra/group_power/lemmas): sign of even/odd powers (#5990)

benjamindavidson committed 4 years ago

ff05d3af

refactor(linear_algebra,algebra/algebra): generalize `linear_map.smul_right` (#5967)

urkud committed 4 years ago

25c34e04

Older