leanprover-community/mathlib3

Pull Requests Commits

Merge branch 'master' into eric-wieser/free_algebra-grading

eric-wieser committed 5 years ago

Verified 7c580605

feat(field_theory/adjoin): induction on adjoin (#5173)

tb65536 committed 5 years ago

30467f4b

chore(algebra/ring): delete a duplicate instance (#5215)

alexjbest committed 5 years ago

7e307bcc

feat(category_theory/limits): cleanup equalizers (#5214)

b-mehta committed 5 years ago

2d00ba48

feat(category_theory/limits): reflects limit if reflects iso and preserves (#5213)

b-mehta committed 5 years ago

b2f8c4c0

chore(topology/continuous_on): change type of `continuous_on.comp_continuous` (#5209)

urkud committed 5 years ago

cfd01f9d

refactor(data/polynomial/derivative): change `polynomial.derivative` to be a `linear_map` (#5198)

awainverse committed 5 years ago

ad25cacf

feat(category_theory/monad): cleanups in monad algebra (#5193)

b-mehta committed 5 years ago

240f6eb9

feat(ring_theory/polynomial/cyclotomic): add order_of_root_cyclotomic (#5151)

riccardobrasca committed 5 years ago

c10d1b1f

feat(category_theory/limits/preserves): preserving terminal objects (#5060)

b-mehta committed 5 years ago

c939c9e4

feat(ring_theory/polynomial/cyclotomic): Möbius inversion formula for cyclotomic polynomials (#5192)

awainverse committed 5 years ago

4f5046dd

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

leanprover-community-bot committed 5 years ago

57dd302d

feat(algebra/lie/basic): define missing inclusion maps (#5207)

Oliver Nash committed 5 years ago

20cc59d9

feat(topology/algebra/order): continuity of monotone functions (#5199)

urkud committed 5 years ago

ec839ef0

doc(tactic/library_search): use more detailed doc string in docs (#5206)

robertylewis committed 5 years ago

3894503e

feat(topology/category/Profinite): add category of profinite top. spaces (#5147)

kbuzzard committed 5 years ago

d416ad69

feat(field_theory/minimal_polynomial): add algebra_map_inj (#5062)

riccardobrasca committed 5 years ago

6f38a50d

fix(linear_algebra/multilinear): Fix incorrect type constraints on `dom_dom_congr` (#5203)

eric-wieser committed 5 years ago

986cabf3

chore(linear_algebra/determinant): Move some lemmas about swaps to better files (#5201)

eric-wieser committed 5 years ago

52697178

feat(group_theory/order_of_element): add is_cyclic_of_prime_card (#5172)

shingtaklam1324 committed 5 years ago

8ff9c0e6

feat(algebra/module/basic): Add smul_comm_class instances (#5205)

eric-wieser committed 5 years ago

f1b387f8

feat(field_theory/separable): is_separable_of_alg_hom_is_separable (#5175)

tb65536 committed 5 years ago

a4b6c418

refactor(field_theory/fixed): Generalize alg_hom lemmas (#5174)

tb65536 committed 5 years ago

b978f366

feat(ring_theory/witt_vector/frobenius): the frobenius endomorphism of witt vectors (#4838)

jcommelin committed 5 years ago

e7c2bba1

feat(ring_theory/witt_vector): witt_sub, a demonstration of is_poly techniques (#5165)

jcommelin committed 5 years ago

f1531ea5

feat(group_theory/group_action/sub_mul_action): Add an object for bundled sets closed under a mul action (#4996)

eric-wieser committed 5 years ago

f6273d4d

feat(combinatorics/simple_graph/matching): introduce matchings and perfect matchings of graphs (#5156)

agusakov committed 5 years ago

98a20c25

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

leanprover-community-bot committed 5 years ago

61e76c42

chore(topology/algebra/ordered): add `order_iso.to_homeomorph` (#5111)

urkud committed 5 years ago

d9a7d05d

feat(category_theory/monad): mark monad lemmas as reassoc (#5190)

b-mehta committed 5 years ago

3f61e549

Older