leanprover-community/mathlib3

Pull Requests Commits

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

kim-em committed 5 years ago

abb3121f

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

kim-em committed 5 years ago

f153a85a

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

urkud committed 5 years ago

c7a2d670

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

kim-em committed 5 years ago

cc3e2c77

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

leanprover-community-bot committed 5 years ago

ee1947d7

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

b-mehta committed 5 years ago

5b18369a

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

kex-y committed 5 years ago

11f18015

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

Julian-Kuelshammer committed 5 years ago

9668bdd5

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

b-mehta committed 5 years ago

09d572d7

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

Julian-Kuelshammer committed 5 years ago

aa0b274b

feat(ring_theory/power_series/basic): coeff_zero_X_mul (#6445)

mo271 committed 5 years ago

d1b7a676

feat(data/option): add `option.forall` and `option.exists` (#6419)

urkud committed 5 years ago

a19af600

feat(tactic/apply_fun): work on the goal as well (#6439)

kim-em committed 5 years ago

4b02853b

chore(data/nat/choose): fix namespace of theorems (#6451)

kim-em committed 5 years ago

7256361a

feat(ring_theory/power_series/basic): rescale_inj (#6446)

mo271 committed 5 years ago

5f68d0e5

feat(algebra/homology/chain_complex): pushforward of complex w.r.t. additive functor (#6403)

adamtopaz committed 5 years ago

f33418a9

feat(category_theory/skeletal): skeleton of a general category (#6443)

b-mehta committed 5 years ago

7ce01bbc

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

leanprover-community-bot committed 5 years ago

1af882b4

feat(category_theory/monoidal): construct the monoidal inverse to a functor (#6442)

b-mehta committed 5 years ago

d38b5a50

feat(linear_algebra/basic): add is_scalar_tower instance for hom type (#6331)

kbuzzard committed 5 years ago

a225e12c

feat(algebra/lie/solvable): images of solvable Lie algebras are solvable (#6413)

ocfnash committed 5 years ago

407615e0

feat(category_theory/subobject): kernels and images as subobjects (#6301)

kim-em committed 5 years ago

ddefd965

feat(data/equiv/basic): Add `fin_succ_above_equiv` (#5145)

eric-wieser committed 5 years ago

11e1cc36

feat(linear_algebra/tensor_product): allow different semirings in linear_map.flip (#6414)

eric-wieser committed 5 years ago

20b49fbd

feat(algebra/big_operators): add lemmas about `sum` and `pi.single` (#6390)

urkud committed 5 years ago

47b62ea4

feat(topology/instances/real, topology/metric_space/basic, algebra/floor): integers are a proper space (#6437)

hrmacbeth committed 5 years ago

aeda3fb7

chore(data/finsupp/basic): add coe_{neg,sub,smul} lemmas to match coe_{zero,add,fn_sum} (#6350)

eric-wieser committed 5 years ago

ff5fa529

feat(algebraic_topology): introduce the simplex category (#6173)

kim-em committed 5 years ago

dd5363b5

feat(polynomial/eval): lemmas relating eval/map on numerals (#6438)

kim-em committed 5 years ago

2f1de3f7

feat(analysis/complex/basic): complex conjugation is a linear isometry (#6436)

hrmacbeth committed 5 years ago

300e81de

Newer Older