leanprover-community/mathlib3

Pull Requests Commits

kbuzzard committed 3 years ago

359a122b

Merge branch 'master' into kbuzzard-order-ideal-gc

kbuzzard committed 3 years ago

93a9e77e

chore(ring_theory/polynomial/symmetric): golf proofs (#14866)

eric-wieser committed 3 years ago

416edbd3

fix(meta/expr): remove `has_reflect.has_to_pexpr` (#14901)

eric-wieser committed 3 years ago

c45e5d58

chore(analysis/special_functions/log/basic): golf a proof (#14898)

urkud committed 3 years ago

2a732ed5

feat(order/filter/basic): add some lemmas about `eventually_le` (#14891)

kex-y committed 3 years ago

23918a54

refactor(data/set/countable): make `set.countable` protected (#14886)

urkud committed 3 years ago

12e5f2e0

refactor(data/finite/card): split from `basic` (#14885)

urkud committed 3 years ago

d8fc588d

feat(topology/basic): `sum.elim` of locally finite set families is locally finite (#14826)

urkud committed 3 years ago

c2719adf

feat({algebra/big_operators/basic,data/rat/cast}): Missing cast lemmas (#14824)

YaelDillies committed 3 years ago

44bb35e5

chore(data/rat): rename `data.rat.basic` to `data.rat.defs` (#14895)

Vierkantor committed 3 years ago

38642efc

chore(algebra/{group_power,order}): split off field lemmas (#14849)

Vierkantor committed 3 years ago

f57c0cdc

feat(topology/vector_bundle/hom): define the vector bundle of continuous linear maps (#14541)

fpvandoorn committed 3 years ago

d939b0e6

feat(set_theory/surreal/basic): define map `surreal →+o game` (#14783)

vihdzp committed 3 years ago

ad497685

feat(combinatorics/simple_graph/connectivity): Connectivity is a graph property (#14865)

YaelDillies committed 3 years ago

61b837fb

fix(tactic/apply_fun.lean): instantiate mvars in apply_fun (#14882)

digama0 committed 3 years ago

f3cd150b

chore(linear_algebra/alternating): more lemmas about `curry_left` (#14844)

eric-wieser committed 3 years ago

3b6552e0

feat(data/finsupp/basic): make `prod_add_index_of_disjoint` to_additive (#14786)

stuart-presnell committed 3 years ago

d9537732

feat(data/sigma): add reflected instance (#14764)

eric-wieser committed 3 years ago

3e66afe7

feat(order/conditionally_complete_lattice): add `cInf_le_cInf'` (#14719)

user7230724 committed 3 years ago

b779513a

golf(data/polynomial): factorization into linear factors when #roots=degree (#14862)

alreadydone committed 3 years ago

2d70b946

feat(topology/metric_space/basic): Add `ball_comm` lemmas (#14858)

linesthatinterlace committed 3 years ago

ee123628

doc(data/polynomial/div): fix runaway code block (#14864)

eric-wieser committed 3 years ago

2b5a5770

feat(ring_theory/dedekind_domain/ideal): drop an unneeded assumption (#14444)

urkud committed 3 years ago

65031caf

fix(topology/algebra/group_completion): add lemmas about nsmul and zsmul and fix diamonds (#14846)

eric-wieser committed 3 years ago

273986ad

feat(data{finset,set}/pointwise): Pointwise monoids are domains (#14687)

YaelDillies committed 3 years ago

2a7bde04

refactor(algebra/{hom/equiv, ring/equiv}): rename `equiv_of_unique_of_unique` to `equiv_of_unique` (#14861)

vihdzp committed 3 years ago

481f9910

chore(set_theory/game/*): create `pgame` and `natural_ops` locales (#14856)

vihdzp committed 3 years ago

e1d7cc70

fix(tactic/norm_num): fix bad proof / bad test (#14852)

digama0 committed 3 years ago

67e026c8

chore(data/finsupp/fin): fix spacing (#14860)

vihdzp committed 3 years ago

8ac19d32

Older