leanprover-community/mathlib3

Pull Requests Commits

feat(number_theory/bernoulli): bernoulli_poly_eval_one (#6581)

mo271 committed 5 years ago

49afae5a

feat(linear_algebra/pi): add `submodule.pi` (#6576)

urkud committed 5 years ago

98895022

feat(analysis/normed_space/normed_group_hom): bounded homs between normed groups (#6375)

jcommelin committed 5 years ago

a3311136

Make to_mul and to_add reducible.

gebner committed 5 years ago

63c1a248

Add normalization lemmas.

gebner committed 5 years ago

3f2dda02

chore(topology/algebra/ordered): use dot notation, golf some proofs (#6595)

urkud committed 5 years ago

6dec23b2

refactor(topology/bounded_continuous_function): structure extending continuous_map (#6521)

kim-em committed 5 years ago

32bd00f1

gebner committed 5 years ago

1964f73a

feat(algebra/continued_fractions) add determinant formula and approximations for error term (#6461)

kappelmann committed 5 years ago

3e5d90d9

feat(linear_algebra): submodules of f.g. free modules are free (#6178)

Vierkantor committed 5 years ago

0afdaab2

Merge remote-tracking branch 'origin/master' into add-mult-struct

gebner committed 5 years ago

fe4034ef

Add some documentation.

gebner committed 5 years ago

045a1580

chore(topology): add a few simple lemmas (#6580)

urkud committed 5 years ago

cdc222da

feat(linear_algebra/bilinear_form): Existence of orthogonal basis with respect to a bilinear form (#5814)

kex-y committed 5 years ago

87eec0b6

Merge remote-tracking branch 'origin/add-mult-struct' into add-mult-struct

gebner committed 5 years ago

f11c5c04

Merge remote-tracking branch 'origin/master' into add-mult-struct

gebner committed 5 years ago

31a584ef

chore(algebra/module/linear_map): add linear_map.to_distrib_mul_action_hom (#6573)

eric-wieser committed 5 years ago

6791ed9b

chore(algebra/monoid_algebra): provide finer-grained levels of structure for less-structured `G`. (#6572)

eric-wieser committed 5 years ago

13d86df6

feat(linear_algebra/{bilinear,quadratic}_form): inherit scalar actions from algebras (#6586)

eric-wieser committed 5 years ago

7058fa61

feat(algebra/algebra/{basic,tower}): add alg_equiv.comap and alg_equiv.restrict_scalars (#6548)

eric-wieser committed 5 years ago

5d0a40f1

feat(algebraic_topology): simplicial objects and simplicial types (#6195)

kim-em committed 5 years ago

b6ed62ca

feat(bounded_continuous_function): coe_sum (#6522)

kim-em committed 5 years ago

f3dbe9f0

feat(data/set/function): three lemmas about maps_to (#6518)

eric-wieser committed 5 years ago

98c6bbc9

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

leanprover-community-bot committed 5 years ago

5b61f07f

feat(order/ideal): added proper ideal typeclass and lemmas to order_top (#6566)

atarnoam committed 5 years ago

2d3c522b

Merge branch 'master' into add-mult-struct

eric-wieser committed 5 years ago

Verified 9c666f60

feat(algebra/regular): add lemmas about regularity of non-zero elements (#6579)

adomani committed 5 years ago

79be90a7

feat(number_theory/bernoulli): definition and properties of Bernoulli polynomials (#6309)

laughinggas committed 5 years ago

b25994d5

fead(data/support): add `support_smul` (#6569)

urkud committed 5 years ago

d9370e03

refactor(geometry/manifold): drop some unused arguments (#6545)

urkud committed 5 years ago

02251b1e

Newer Older