leanprover-community/mathlib

Pull Requests Commits

chore(group_theory/submonoid/operations): use coercion instead of .val

eric-wieser committed 4 years ago

4bfeb0d2

feat(analysis/convex): linear image of segment (#6531)

b-mehta committed 4 years ago

9607dbdd

feat(algebra/direct_sum_graded): endow `direct_sum` with a ring structure (#6053)

eric-wieser committed 4 years ago

a8d285cc

doc(group_theory/sylow): module doc (#6477)

Julian-Kuelshammer committed 4 years ago

edbbecbe

feat(data/finsupp/basic): add support_nonempty_iff and nonzero_iff_exists (#6530)

adomani committed 4 years ago

d32bb6ed

feat(linear_algebra/clifford_algebra): add definitions of the conjugation operators and some API (#6491)

eric-wieser committed 4 years ago

ca96bfbe

feat(data/mv_polynomial/equiv): generalize ring_equiv_congr (#6420)

riccardobrasca committed 4 years ago

deb3d452

chore(topology/algebra/*): tendsto namespacing (#6528)

hrmacbeth committed 4 years ago

3329ec4e

refactor(big_operators/basic): move prod_mul_prod_compl (#6526)

kim-em committed 4 years ago

76aee25d

feat(topology/instances/real): generalize 'compact_space I' to 'compact_space (Icc a b)' (#6523)

kim-em committed 4 years ago

d7fa1bc8

chore(*/sub*): tidy up inherited algebraic structures from parent objects (#6509)

eric-wieser committed 4 years ago

2f357794

feat(category_theory/subobject): factoring morphisms through subobjects (#6302)

kim-em committed 4 years ago

f4db322f

feat(algebra/star): the Bell/CHSH/Tsirelson inequalities (#4687)

kim-em committed 4 years ago

8289518d

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

leanprover-community-bot committed 4 years ago

28378076

chore(algebra/ordered_group): put to_additive on lemmas about linear_ordered_comm_group (#6506)

eric-wieser committed 4 years ago

3c9399d1

feat(data/list/basic): add `list.prod_eq_zero(_iff)` (#6504)

urkud committed 4 years ago

d4ac4c3e

feat(data/equiv/fin): fin_add_flip and fin_rotate (#6454)

kim-em committed 4 years ago

a852bf40

chore(ring_theory/{subring,integral_closure}): simplify a proof, remove redundant instances (#6513)

eric-wieser committed 4 years ago

9c48eb18

feat(algebra/field): add function.injective.field (#6511)

eric-wieser committed 4 years ago

eec54d05

refactor(ring_theory/polynomial/chebyshev): move lemmas around (#6510)

hrmacbeth committed 4 years ago

3309ce27

chore(data/equiv): add missing simp lemmas about mk (#6505)

eric-wieser committed 4 years ago

383dd2bd

feat(algebra/big_operators/basic): lemmas prod_range_add, sum_range_add (#6484)

Nazgand committed 4 years ago

22e34370

refactor(ring_theory/valuation): valuations in `linear_ordered_comm_monoid_with_zero` (#6500)

awainverse committed 4 years ago

19ed0f8e

feat(ring_theory/polynomial/chebyshev/basic): multiplication of Chebyshev polynomials (#6501)

hrmacbeth committed 4 years ago

0c5b5172

refactor(data/set/finite): change type of `set.finite.dependent_image` (#6475)

urkud committed 4 years ago

0c863e98

refactor(data/set/finite): make `finite` argument of `set.finite.mem_to_finset` explicit (#6508)

urkud committed 4 years ago

c0870115

feat(data/{nat,int}/parity): even_mul_succ_self (#6507)

pechersky committed 4 years ago

9f0f05ee

feat(data/finset/lattice): +2 induction principles for `finset`s (#6502)

urkud committed 4 years ago

6b5e48d7

chore(algebra/big_operators): use weaker typeclass assumptions (#6503)

urkud committed 4 years ago

572f7274

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

leanprover-community-bot committed 4 years ago

c69c8a9e

Older