leanprover-community/mathlib

Pull Requests Commits

adomani committed 3 years ago

cf16ca80

add file algebra/order/cov_semiring

adomani committed 3 years ago

131a3ec5

fix(tactic/suggest): make `library_search` aware of definition of `ne` (#11742)

arthurpaulino committed 3 years ago

50cdb957

fix(tactic/squeeze_simp): "match failed" when `simp` works (#11659)

ericrbg committed 3 years ago

07735b8a

chore(ring_theory/polynomial/chebyshev): simplify argument using new `linear_combination` tactic (#11736)

hrmacbeth committed 3 years ago

b0fc10a1

feat(group_theory/sylow): preimages of sylow groups (#11722)

nomeata committed 3 years ago

97f61dfd

chore(*): Rename `prod_dvd_prod` (#11734)

stuart-presnell committed 3 years ago

02c720ee

feat(data/pnat/basic): 0 < n as a fact (#11729)

ericrbg committed 3 years ago

a248befb

chore(ring_theory/localization) weaken hypothesis from field to comm_ring (#11713)

ChrisHughes24 committed 3 years ago

dde904e0

feat(tactic/linear_combination): add tactic for combining equations (#11646)

agoldb10 committed 3 years ago

1ea49d0f

chore(analysis/normed_space/star): create new folder for normed star rings (#11732)

dupuisf committed 3 years ago

73e45c62

chore(measure_theory/function/conditional_expectation): fix typo (#11731)

kex-y committed 3 years ago

09d4f485

feat(field_theory/ratfunc): rational functions as Laurent series (#11276)

pechersky committed 3 years ago

af1290cb

feat(analysis/convex/topology): add lemmas (#11615)

urkud committed 3 years ago

ff352187

feat(number_theory/prime_counting): The prime counting function (#9080)

BoltonBailey committed 3 years ago

4085363d

chore(representation_theory/maschke): remove recover (#11721)

ericrbg committed 3 years ago

74250a0a

feat(data/fintype/order): `bool` is a boolean algebra (#11694)

YaelDillies committed 3 years ago

49b8b91a

feat(measure_theory/group/basic): make is_[add|mul]_[left|right]_invariant classes (#11655)

fpvandoorn committed 3 years ago

fc4e471b

feat(analysis/inner_product_space): proof of the Lax Milgram theorem (#11491)

danrocag committed 3 years ago

44105f84

chore(ring_theory/polynomial/tower): weaken comm_semiring hypothesis to semiring (#11712)

ChrisHughes24 committed 3 years ago

f51d6bfd

feat(data/nat/mul_ind): generalise rec_on_prime to assume positivity (#11714)

b-mehta committed 3 years ago

601ea914

feat(number_theory/cyclotomic/zeta): add is_cyclotomic_extension.zeta (#11695)

riccardobrasca committed 3 years ago

d58ce5ac

feat(analysis/complex): removable singularity theorem (#11686)

urkud committed 3 years ago

02c31460

refactor(algebra/linear_ordered_comm_group_with_zero, *): mostly take advantage of the new classes for `linear_ordered_comm_group_with_zero` (#7645)

adomani committed 3 years ago

7e8cb757

feat(data/fintype/order): More and better instances (#11702)

YaelDillies committed 3 years ago

dddf6ebe

feat(algebra/ne_zero): add `coe_trans` instance (#11700)

ericrbg committed 3 years ago

6ca08e81

feat(algebra/big_operators/{basic,multiset}): two `multiset.prod` lemmas (#11693)

stuart-presnell committed 3 years ago

de27bfc8

feat(analysis/convex/specific_functions): sin is strictly concave (#11688)

b-mehta committed 3 years ago

c50a60de

feat(group_theory/nilpotent): add upper_central_series_eq_top_iff_nilpotency_class_le (#11670)

nomeata committed 3 years ago

92c64c45

feat(topology/continuous_function/algebra): `C(α, β)` is a topological group (#11665)

tb65536 committed 3 years ago

7a485b1b

Older