leanprover-community/mathlib

Pull Requests Commits

Merge branch 'master' into cc-lifting

b-mehta committed 4 years ago

Verified cd32d0ff

feat(ring_theory/jacobson): Generalize proofs about Jacobson rings and polynomials (#5520)

dtumad committed 4 years ago

55d5564a

feat(algebra/category/Module): direct limit is a colimit (#4756)

jcommelin committed 4 years ago

05e7be9d

feat(ring_theory/algebra_tower): Restriction of adjoin (#5767)

tb65536 committed 4 years ago

f03f5a96

feat(field_theory/adjoin): Inductively construct algebra homomorphism (#5765)

tb65536 committed 4 years ago

e95988a3

feat(order/closure): closure operator from galois connection (#5764)

b-mehta committed 4 years ago

9acd3496

refactor(ring_theory): change field instance on adjoin_root (#5759)

tb65536 committed 4 years ago

51ffdd03

feat(linear_algebra/{clifford,exterior,tensor,free}_algebra): provide canonical images from larger algebras into smaller ones (#5745)

eric-wieser committed 4 years ago

dffb09ad

feat(category_theory/monad): construct isomorphisms of algebras (#5678)

b-mehta committed 4 years ago

bea76514

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

leanprover-community-bot committed 4 years ago

592edb6b

chore(algebra/group_with_zero): cleanup (#5762)

urkud committed 4 years ago

6351f01d

chore(data/real/*): rename `le_of_forall_epsilon_le` to `le_of_forall_pos_le_add` (#5761)

urkud committed 4 years ago

798024a9

feat(data/nat/modeq): add missing lemmas for int and nat regarding dvd (#5752)

Julian-Kuelshammer committed 4 years ago

78493c9d

feat(group_theory/perm/sign): exists_pow_eq_of_is_cycle (#5665)

tb65536 committed 4 years ago

e4da493c

feat(analysis/analytic/basic): `f (x + y) - p.partial_sum n y = O(∥y∥ⁿ)` (#5756)

urkud committed 4 years ago

d43f202f

feat(data/matrix/notation,data/fin): head and append simp (#5741)

pechersky committed 4 years ago

bc5d5c9d

feat(order/atoms): further facts about atoms, coatoms, and simple lattices (#5493)

awainverse committed 4 years ago

0104948e

fix(algebra/ordered_monoid): Ensure that `ordered_cancel_comm_monoid` can provide a `cancel_comm_monoid` instance (#5713)

eric-wieser committed 4 years ago

bc94d052

feat(data/mv_polynomial): stronger `degrees_X` for `nontrivial R` (#5758)

eric-wieser committed 4 years ago

8b4b9413

feat(algebra/lie/basic): add a few `simp` lemmas (#5757)

ocfnash committed 4 years ago

c347c75d

feat(analysis/calculus/inverse): a map that has an invertible strict derivative at every point is an open map (#5753)

urkud committed 4 years ago

ed0ae3e7

feat(data/complex/basic): Adding `im_eq_sub_conj` (#5750)

JamesAMaths committed 4 years ago

4c1d12f5

chore(linear_algebra/quadratic_form): Add missing simp lemmas about quadratic_form.polar (#5748)

eric-wieser committed 4 years ago

94f45c74

feat(category_theory/over): epis and monos in the over category (#5684)

b-mehta committed 4 years ago

09c23456

feat(category_theory): subterminal objects (#5669)

b-mehta committed 4 years ago

395eb2ba

feat(category_theory/limits): finite products from binary products (#5516)

b-mehta committed 4 years ago

f8db86a2

refactor(data/real/{e,}nnreal): reuse generic lemmas (#5751)

urkud committed 4 years ago

faf106a3

chore(algebra/ordered_ring): add a few simp lemmas (#5749)

urkud committed 4 years ago

931182ee

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

leanprover-community-bot committed 4 years ago

5d003d85

chore(data/equiv/basic): equiv/perm_congr simp lemmas (#5737)

pechersky committed 4 years ago

7151fb70

Older