leanprover-community/mathlib3

Pull Requests Commits

deduplicate `associated` and `associated'`

eric-wieser committed 4 years ago

cbc58d6b

update material from #5814

hrmacbeth committed 4 years ago

a473eb19

hrmacbeth committed 4 years ago

55bb06a1

Apply suggestions from code review

hrmacbeth committed 4 years ago

Verified 086d67c6

Merge remote-tracking branch 'origin/master' into quadratic_form_comm_ring

hrmacbeth committed 4 years ago

3b4d6140

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

urkud committed 4 years ago

cdc222da

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

kex-y committed 4 years ago

87eec0b6

Merge remote-tracking branch 'origin/master' into quadratic_form_comm_ring

hrmacbeth committed 4 years ago

01bab365

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

eric-wieser committed 4 years ago

6791ed9b

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

eric-wieser committed 4 years ago

13d86df6

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

eric-wieser committed 4 years ago

7058fa61

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

eric-wieser committed 4 years ago

5d0a40f1

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

kim-em committed 4 years ago

b6ed62ca

feat(bounded_continuous_function): coe_sum (#6522)

kim-em committed 4 years ago

f3dbe9f0

hrmacbeth committed 4 years ago

cf224607

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

eric-wieser committed 4 years ago

98c6bbc9

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

leanprover-community-bot committed 4 years ago

5b61f07f

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

atarnoam committed 4 years ago

2d3c522b

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

adomani committed 4 years ago

79be90a7

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

laughinggas committed 4 years ago

b25994d5

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

urkud committed 4 years ago

d9370e03

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

urkud committed 4 years ago

02251b1e

feat(analysis/normed_space/multilinear): a few more bundled (bi)linear maps (#6546)

urkud committed 4 years ago

ebe2c616

feat(analysis/special_functions/integrals): mul/div by a const (#6357)

benjamindavidson committed 4 years ago

9f17db51

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

leanprover-community-bot committed 4 years ago

07fc9821

refactor(data/{finset,multiset}): move inductions proofs on sum/prod from finset to multiset, add more induction lemmas (#6561)

RemyDegenne committed 4 years ago

df1e6f92

feat(data/set/basic): add `set.set_ite` (#6557)

urkud committed 4 years ago

b280b005

chore(geometry/manifold): use `namespace`, rename `image` to `image_eq` (#6517)

urkud committed 4 years ago

ac8a1196

feat(order/filter/*, topology/subset_properties): define "coproduct" of two filters (#6372)

hrmacbeth committed 4 years ago

16ef2913

feat(topology/paracompact): define paracompact spaces (#6395)

urkud committed 4 years ago

0fa0d61e

Older