leanprover-community/mathlib

Pull Requests Commits

feat(linear_algebra/basic): simp lemmas about endomorphisms (#6452)

kim-em committed 4 years ago

f63069f3

feat(analysis/special_functions/integrals): some simple integration lemmas (#6216)

benjamindavidson committed 4 years ago

5c016137

feat(data/polynomial): lemmas about polynomial derivative (#6433)

kim-em committed 4 years ago

5eb7ebbb

ci(scripts/detect_errors): try to show info messages in a way github understands (#6493)

eric-wieser committed 4 years ago

03344754

feat(src/order/basic): show injectivity of order conversions, and tag lemmas with ext (#6490)

eric-wieser committed 4 years ago

0a5f69cc

chore(data/equiv/basic): add simp lemmas about subtype_equiv (#6479)

eric-wieser committed 4 years ago

cc579154

feat(linear_algebra/finsupp): add mem_span_set (#6457)

adomani committed 4 years ago

354fda08

feat(ring_theory/finiteness): improve API for finite presentation (#6382)

riccardobrasca committed 4 years ago

e0a4dd88

feat(ring_theory/hahn_series): introduce ring of Hahn series (#6237)

awainverse committed 4 years ago

0faa7880

feat(linear_algebra/{clifford,exterior,tensor}_algebra): add induction principles (#6416)

eric-wieser committed 4 years ago

e77f071c

fix(group_action/defs): make mul_action.regular an instance (#6241)

eric-wieser committed 4 years ago

aff6bd1b

doc(algebra/ring/basic): change pullback and injective to pushforward and surjective (#6487)

adomani committed 4 years ago

6ac19b46

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

leanprover-community-bot committed 4 years ago

9ad469d8

feat(geometry/manifold): `ext_chart_at` is smooth on its source (#6473)

urkud committed 4 years ago

13f30e53

feat(category_theory/monoidal): skeleton of a monoidal category is a monoid (#6444)

b-mehta committed 4 years ago

83bc6634

feat(analysis/calculus): Lagrange multipliers (#6431)

urkud committed 4 years ago

1e45472a

chore(category/equivalence): remove functor.fun_inv_id (#6450)

kim-em committed 4 years ago

18804b20

feat(archive/100-theorems-list/9_area_of_a_circle): area of a disc (#6374)

JamesAMaths committed 4 years ago

ac3c4787

feat(data/set): more lemmas (#6474)

urkud committed 4 years ago

b1818660

feat(analysis/special_functions/pow): smoothness of `complex.cpow` (#6447)

urkud committed 4 years ago

ef5c1d50

chore(*): more line lengths (#6472)

kim-em committed 4 years ago

abb3121f

chore(category_theory/*): fix long lines (#6471)

kim-em committed 4 years ago

f153a85a

refactor(analysis/calculus/specific_functions): add params to `smooth_bump_function` (#6467)

urkud committed 4 years ago

c7a2d670

feat(linear_algebra/basic): f x ∈ submodule.span R (f '' s) (#6453)

kim-em committed 4 years ago

cc3e2c77

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

leanprover-community-bot committed 4 years ago

ee1947d7

feat(ring_theory/power_series): coeff multiplication lemmas (#6462)

b-mehta committed 4 years ago

5b18369a

feat(linear_algebra/quadratic_form): add associated_eq_self_apply (#6458)

kex-y committed 4 years ago

11f18015

feat(algebra/category/Mon/adjunctions): adjoin_unit adjunction from Semigroup (#6440)

Julian-Kuelshammer committed 4 years ago

9668bdd5

feat(algebra/big_operators): additive versions of multiset lemmas (#6463)

b-mehta committed 4 years ago

09d572d7

chore(*): split lines and move module doc `measure_theory/category/Meas` (#6459)

Julian-Kuelshammer committed 4 years ago

aa0b274b

Newer Older