leanprover-community/mathlib3

Pull Requests Commits

fpvandoorn committed 2 years ago

2698120b

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

feat(linear_algebra/finite_dimensional): generalize results to `module.finite` (#18811)

eric-wieser committed 2 years ago

e95e4f92

feat(algebra/order/sub/defs): make `has_ordered_sub` a Prop (#18810)

kbuzzard committed 2 years ago

de29c328

feat(data/matrix/basic): more lemmas about submatrix (#18738)

eric-wieser committed 2 years ago

0e2aab2b

feat(analysis/calculus/cont_diff_def): no continuity is needed for has_ftaylor_series_up_to if n = ∞ (#18808)

mcdoll committed 2 years ago

2cf3ee29

feat(data/matrix/reflection): add `mul_vec` and `vec_mul` (#18805)

eric-wieser committed 2 years ago

820b2296

chore(analysis/seminorm): add new le_def/lt_def and renaming (#18801)

mcdoll committed 2 years ago

7ebf83ed

refactor(linear_algebra/matrix/rank): remove `decidable_eq` arguments (#18800)

eric-wieser committed 2 years ago

86add5ce

chore(linear_algebra/free_module/rank): golf a slow proof (#18804)

eric-wieser committed 2 years ago

465d4301

feat(data/matrix/rank): rank of multiplication (#18784)

eric-wieser committed 2 years ago

47a5f818

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

leanprover-community-bot committed 2 years ago

9a48a083

feat(data/matrix/rank): rank of a matrix is the rank of its column space (#18778)

eric-wieser committed 2 years ago

21407283

chore(linear_algebra/matrix/dot_product): weaken typeclasses (#18798)

eric-wieser committed 2 years ago

5ac1dab1

chore(linear_algebra/finrank): backport removal of simp lemmas (#18794)

kim-em committed 2 years ago

347636a7

feat(linear_algebra/free_module/finite/rank): remove `module.free` assumption (#18792)

eric-wieser committed 2 years ago

b5b5dd5a

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

leanprover-community-bot committed 2 years ago

814d76e2

chore(set_theory/cardinal/basic): reinstate `partial_order` (#18781)

vihdzp committed 2 years ago

9bb28972

feat(linear_algebra/matrix/dot_product): `dot_product_self_eq_zero` (#18783)

eric-wieser committed 2 years ago

46822d96

chore(ring_theory/finiteness): generalize `finite_dimensional_range` to modules (#18787)

eric-wieser committed 2 years ago

039ef89b

Older