leanprover-community/mathlib

Pull Requests Commits

Use the notation

eric-wieser committed 4 years ago

2b3cfe7b

feat(linear_algebra/multilinear): add notation

eric-wieser committed 4 years ago

295d20e3

refactor(order/closure): golf `closure_inter_le` (#6138)

Jesse Michael Han committed 4 years ago

5a2eac67

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

leanprover-community-bot committed 4 years ago

0731a700

chore(group_theory/perm/sign): speed up sign_aux_swap_zero_one proof (#6128)

pechersky committed 4 years ago

922ecb07

chore(data/fin): reorder file to group declarations (#6109)

pechersky committed 4 years ago

18b378d8

feat(data/equiv/mul_add): monoids/rings with one element are isomorphic (#6079)

kbuzzard committed 4 years ago

4c1c11ce

feat(algebra/geom_sum): adds further variants (#6077)

Julian-Kuelshammer committed 4 years ago

b34da002

feat(measure_theory/lp_space): add more API on Lp spaces (#6042)

sgouezel committed 4 years ago

49e50ee5

feat(category_theory/monad): use bundled monads everywhere (#5889)

b-mehta committed 4 years ago

7c77279e

refactor(algebra/lie/basic): rm extraneous rewrite hypothesis (#6137)

Jesse Michael Han committed 4 years ago

ba9e06ec

refactor(measure_theory/measure_space): simplify proof (#6136)

Jesse Michael Han committed 4 years ago

456bdb73

refactor(ring_theory/polynomial/symmetric): simplify proof (#6135)

Jesse Michael Han committed 4 years ago

c377e68e

refactor(*): remove uses of omega in the library (#6129)

sgouezel committed 4 years ago

eb2dcba5

refactor(data/string/basic): simplify proof of `to_list_nonempty` (#6117)

Jesse Michael Han committed 4 years ago

296899eb

feat(analysis/special_functions/trigonometric): `complex.log` is smooth away from `(-∞, 0]` (#6041)

urkud committed 4 years ago

d9d56eb3

refactor(analysis/special_functions/trigonometric): simpler proof (#6133)

Jesse Michael Han committed 4 years ago

e8f383c0

refactor(data/fintype/basic): golf `card_eq_one_of_forall_eq` (#6131)

Jesse Michael Han committed 4 years ago

bf1465c2

feat(archive/imo): formalize solution to IMO 2013 problem Q1 (#6110)

dwrensha committed 4 years ago

fdbd4bff

feat(analysis/normed_space/operator_norm): lemmas about `E →L[𝕜] F →L[𝕜] G` (#6102)

urkud committed 4 years ago

aa9e2b8f

fix(topology/algebra/infinite_sum): remove hard-coding of ℕ and ℝ (#6096)

eric-wieser committed 4 years ago

766146b9

refactor(geometry/euclidean): shorten proof (#6121)

Jesse Michael Han committed 4 years ago

2d50cce3

refactor(linear_algebra/prod): split out prod and coprod defs and lemmas (#6059)

eric-wieser committed 4 years ago

aaab1139

feat(group_theory/perm/sign): induced permutation on a subtype that is a fintype (#5706)

paulvanwamelen committed 4 years ago

17448c64

refactor(group_theory/solvable): `simp` -> assumption (#6120)

Jesse Michael Han committed 4 years ago

342bccf6

refactor(data/ordmap/ordset): simpler proof of `not_le_delta` (#6119)

Jesse Michael Han committed 4 years ago

ec8f2ac8

refactor(computability/partrec): simpler proof of `subtype_mk` (#6118)

Jesse Michael Han committed 4 years ago

7e5ff2f1

refactor(category_theory/adjunction/mates): faster proof (#6116)

Jesse Michael Han committed 4 years ago

183f4fce

refactor(combinatorics/simple_graph): simplify proofs (#6115)

Jesse Michael Han committed 4 years ago

1611b30c

refactor(algebra/lie/basic): golf `lie_algebra.morphism.map_bot_iff` (#6114)

Jesse Michael Han committed 4 years ago

d06b11a5

Older