leanprover-community/mathlib3

Pull Requests Commits

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

awainverse committed 5 years ago

cbd67cf4

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

eric-wieser committed 5 years ago

5f328b6e

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

adomani committed 5 years ago

36b35107

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

benjamindavidson committed 5 years ago

360fa07e

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

urkud committed 5 years ago

bb15b1ce

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

robertylewis committed 5 years ago

235a7c46

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

benjamindavidson committed 5 years ago

9a0d2b23

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

BoltonBailey committed 5 years ago

fa8df59b

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

kex-y committed 5 years ago

5a9ca8d3

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

Julian-Kuelshammer committed 5 years ago

e1ca806c

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

leanprover-community-bot committed 5 years ago

e66ad5f5

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

cemulate committed 5 years ago

79ca6e23

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

alexjbest committed 5 years ago

fcad25f2

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

urkud committed 5 years ago

2153dc34

Delete a stray `#lint`

Vierkantor committed 5 years ago

f0164f3c

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

urkud committed 5 years ago

1b1ad15c

Fix renamed lemmas

Vierkantor committed 5 years ago

dc53ac63

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

urkud committed 5 years ago

2b2edc97

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

eric-wieser committed 5 years ago

4e786548

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

hrmacbeth committed 5 years ago

fe9c021d

Merge branch 'dedekind-domain-dev' of https://github.com/leanprover-community/mathlib into dedekind-domain-dev

faenuccio committed 5 years ago

968e4fd3

removed hNF from coe_ideal_mul_one_div

faenuccio committed 5 years ago

2b9a8552

WIP: get rid of (almost all?) linting issues

Vierkantor committed 5 years ago

8e29f6b0

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

pechersky committed 5 years ago

dbb5ca1e

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

fpvandoorn committed 5 years ago

9b3dc417

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

gebner committed 5 years ago

6633a70e

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

eric-wieser committed 5 years ago

508c2650

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

BoltonBailey committed 5 years ago

3732fb9d

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

benjamindavidson committed 5 years ago

ff05d3af

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

urkud committed 5 years ago

25c34e04

Newer Older