leanprover-community/mathlib3

Pull Requests Commits

chore(data/matrix/basic): make std_basis_matrix a linear map

eric-wieser committed 4 years ago

0107f3f3

feat(analysis/special_functions/trigonometric): add mistakenly omitted lemma (#6036)

benjamindavidson committed 4 years ago

1a2eb0b5

refactor(analysis/normed_space): simpler proof of `norm_sub_pow_two` (#6035)

Jesse Michael Han committed 4 years ago

16be8e39

doc(number_theory/{pell, sum_of_four_squares}): docstring to pell (#6030)

Julian-Kuelshammer committed 4 years ago

894ff7ad

refactor(analysis/asymptotics): make definitions immediately irreducible (#6021)

gebner committed 4 years ago

0aed8b1e

chore(linear_algebra/std_basis): move std_basis to a new file (#6020)

eric-wieser committed 4 years ago

97781b9a

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

Older