leanprover-community/mathlib

Pull Requests Commits

Merge remote-tracking branch 'origin/eric-wieser/better-matrix-notation' into eric-wieser/matrix-wip

eric-wieser committed 3 years ago

6d136046

eric-wieser committed 3 years ago

a33c31c3

Merge remote-tracking branch 'origin/master' into eric-wieser/matrix-wip

eric-wieser committed 3 years ago

4a35135c

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

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

feat(order/monotone): Monotonicity of `prod.map` (#14843)

YaelDillies committed 3 years ago

f855a4ba

feat(logic/unique): functions from a `unique` type is `const` (#14823)

alreadydone committed 3 years ago

66d3f897

docs(linear_algebra): refer to `pi.basis_fun` in `pi.basis` (#14505)

Vierkantor committed 3 years ago

0b806ba6

feat(data/prod/basic): Involutivity of `prod.map` (#14845)

YaelDillies committed 3 years ago

c781c0ea

Older