leanprover-community/mathlib

Pull Requests Commits

chore(linear_algebra/quadratic_form): fix typo (#7907)

kex-y committed 4 years ago

9ad8ea3b

fix(tactic/lint): punctuation of messages (#7869)

fpvandoorn committed 4 years ago

7b7cd0a1

feat(algebra/pointwise): Dynamics of powers of a subset (#7836)

tb65536 committed 4 years ago

39073fa2

feat(topology/category/Profinite/cofiltered_clopen): Theorem about clopen sets in cofiltered limits of profinite sets (#7837)

adamtopaz committed 4 years ago

ee4fe743

feat(linear_algebra/free_module): add class module.free (#7801)

riccardobrasca committed 4 years ago

06094d56

feat(geometry/manifold): Some lemmas for smooth functions (#7752)

Nicknamen committed 4 years ago

f9935ede

chore(ring_theory/adjoin_root): speedup (#7905)

sgouezel committed 4 years ago

b7d4996e

chore(data/nat/sqrt): Alternative phrasings of data.nat.sqrt lemmas (#7748)

Smaug123 committed 4 years ago

15b24348

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

Newer Older