leanprover-community/mathlib3

Pull Requests Commits

Merge branch 'apurva/convex-cone-closure' into apurva/proper-cone

apurvnakade committed 2 years ago

7fc09275

apurvnakade committed 2 years ago

9cdd9ef0

suggestions from code review

apurvnakade committed 2 years ago

feebcb99

fix typo in todo

apurvnakade committed 2 years ago

2825353d

apurvnakade committed 2 years ago

71fe69e5

Merge branch 'master' into apurva/convex-cone-closure

apurvnakade committed 2 years ago

d86e60c4

Apurva Nakade committed 2 years ago

79c38641

Merge branch 'apurva/convex-cone-closure' into apurva/proper-cone

Apurva Nakade committed 2 years ago

c12a72ee

Weaken hypothesis

Apurva Nakade committed 2 years ago

d9dd4a85

Apply suggestions from code review

apurvnakade committed 2 years ago

Verified e401dbab

Apurva Nakade committed 2 years ago

9e366134

Fix typecast error

Apurva Nakade committed 2 years ago

7f3426f9

Fix misplaced bracket.

Apurva Nakade committed 2 years ago

04952319

Fix linter simp error.

Apurva Nakade committed 2 years ago

70b20a1d

Apply suggestions from code review

apurvnakade committed 2 years ago

Verified dee08002

Apurva Nakade committed 2 years ago

998445cd

feat(data/matrix/rank): rank of `Aᵀ ⬝ A` and `Aᴴ ⬝ A` (#18818)

eric-wieser committed 2 years ago

17219820

chore(*): add mathlib4 synchronization comments (#18832)

leanprover-community-bot committed 2 years ago

8eb9c42d

feat(ring_theory/polynomial): define the probabilist's Hermite polynomials (#18739)

lukemantle committed 2 years ago

c6275ef4

chore(data/complex/module): split out orientation to a separate file (#18824)

kim-em committed 2 years ago

cd8fafa2

chore(linear_algebra/matrix/basis): reduce imports (#18823)

kim-em committed 2 years ago

6c263e4b

chore(*): add mathlib4 synchronization comments (#18813)

leanprover-community-bot committed 2 years ago

ce38d86c

feat(topology/perfect): Schemes, embedding of the Cantor space (#18248)

Felix-Weilacher committed 2 years ago

49b7f94a

feat(measure_theory/functions/lp_space): bounds on the sum of functions in L^p, p < 1, and applications (#18796)

sgouezel committed 2 years ago

13bf7613

feat(algebra/module/submodule/basic): add has_vadd (#18815)

xroblot committed 2 years ago

155d5519

golf(set_theory/ordinal/cantor_normal_form): golf theorems (#16009)

vihdzp committed 2 years ago

991ff3b5

feat(analysis/schwartz_space): lemmas for supremum of seminorms (#18648)

mcdoll committed 2 years ago

a968611b

feat(category_theory/site/limits): generalise universes (#18817)

kbuzzard committed 2 years ago

95e83ced

ci: fix bibtool installation (#18816)

eric-wieser committed 2 years ago

17ad94b4

chore(*): add mathlib4 synchronization comments (#18807)

leanprover-community-bot committed 2 years ago

4f4a1c87

Older