leanprover-community/mathlib3

Pull Requests Commits

feat(data/polynomial): generalize `polynomial.has_scalar` to require only `distrib_mul_action` instead of `semimodule` (#7664)

eric-wieser committed 4 years ago

841dce13

feat(linear_algebra): use `finset`s to define `det` and `trace` (#7778)

Vierkantor committed 4 years ago

2016a93a

feat(tactic/{induction,fresh_names}): improve `induction' with` (#7726)

JLimperg committed 4 years ago

dabb41f2

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

leanprover-community-bot committed 4 years ago

55c96623

feat(ring_theory): every division_ring is_noetherian (#7661)

kim-em committed 4 years ago

2974a9f9

feat(ring_theory): the field trace resp. norm is the sum resp. product of the conjugates (#7640)

Vierkantor committed 4 years ago

5948cde7

feat(analysis/special_functions/integrals): integral of `sin x ^ m * cos x ^ n` (#7418)

benjamindavidson committed 4 years ago

43379184

feat(topology/category/Top/limits): Kőnig's lemma for fintypes (#6288)

kmill committed 4 years ago

2d175ae6

chore(src/algebra/lie/abelian): golf (#7898)

adomani committed 4 years ago

b3606111

chore(algebra/{covariant_and_contravariant + ordered_monoid_lemmas}): new file covariant_and_contravariant (#7890)

adomani committed 4 years ago

dd600354

feat(data/finset/basic): `empty_product` and `product_empty` (#7886)

YaelDillies committed 4 years ago

538f015c

doc(data/pequiv): add module docs (#7877)

ericrbg committed 4 years ago

97a7a246

feat({algebra/group_action_hom, data/equiv/mul_add}): add missing `inverse` defs (#7847)

ocfnash committed 4 years ago

ff44ed50

feat(data/finsupp/to_dfinsupp): add sigma_finsupp_lequiv_dfinsupp (#7818)

riccardobrasca committed 4 years ago

a008b33f

feat(ring_theory/adjoin/basic): add subalgebra.fg_prod (#7811)

riccardobrasca committed 4 years ago

64d453ee

feat(algebraic_geometry/structure_sheaf): Define comap on structure sheaf (#7788)

justus-springer committed 4 years ago

61a04c51

feat(linear_algebra/quadratic_form): Real version of Sylvester's law of inertia (#7427)

kex-y committed 4 years ago

eb9bd55f

chore(algebra/{ordered_monoid,linear_ordered_comm_group_with_zero}): remove some uses of @ (#7884)

adomani committed 4 years ago

e8add823

feat(number_theory/l_series): The L-series of an arithmetic function (#7862)

awainverse committed 4 years ago

9500d951

feat(analysis): Cauchy sequence and series lemmas (#7858)

PatrickMassot committed 4 years ago

e35438bb

feat(algebra/periodic): more periodicity lemmas (#7853)

benjamindavidson committed 4 years ago

a4211857

feat(algebra/ordered_group): abs_sub (#7850)

YaelDillies committed 4 years ago

9228ff9c

feat(algebra/order_functions): lt_max_of_lt_<left/right> (#7849)

YaelDillies committed 4 years ago

4bfe8e8a

feat(topology/algebra/ordered/basic): add a few subseq-related lemmas (#7828)

ADedecker committed 4 years ago

915a0a21

chore(algebra/lie/classical): speed up slow proof (#7894)

sgouezel committed 4 years ago

51cd821b

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

leanprover-community-bot committed 4 years ago

6eb3d971

feat(set_theory/cardinal): missing lemma (#7880)

kim-em committed 4 years ago

6f6dbad6

doc(int/modeq): add module doc and tidy (#7878)

ericrbg committed 4 years ago

e8aa9849

chore(data/real/nnreal): avoid abusing inequalities in nnreals (#7872)

adomani committed 4 years ago

1b0e5ee5

feat(logic/function/basic): a lemma on symmetric operations and flip (#7871)

adomani committed 4 years ago

d5705960

Newer Older