leanprover-community/mathlib

Pull Requests Commits

jjaassoonn committed 3 years ago

b250827f

jjaassoonn committed 3 years ago

325d447c

changed to correct definition by Andrew Yang

jjaassoonn committed 3 years ago

f499f81b

add module docstring

jjaassoonn committed 3 years ago

38b5c2e6

add a bunch of definitions

jjaassoonn committed 3 years ago

41855319

unused argument

jjaassoonn committed 3 years ago

7149fc82

jjaassoonn committed 3 years ago

f278f387

jjaassoonn committed 3 years ago

885651c0

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

chore(set_theory/ordinal/natural_ops): use derive (#14859)

vihdzp committed 3 years ago

326465de

feat(data/fintype/basic): equivalence between `finset α` and `set α` for `fintype α` (#14840)

vihdzp committed 3 years ago

3b5441cb

feat(polynomial/ring_division): strengthen/generalize various lemmas (#14839)

alreadydone committed 3 years ago

87f47580

refactor(data/sym/basic): change notation for sym.cons (#14853)

kmill committed 3 years ago

125055b0

chore(data/nat/totient): golf a proof (#14851)

urkud committed 3 years ago

9df2762e

Older