leanprover-community/mathlib3

Pull Requests Commits

YaelDillies committed 2 years ago

cfeef526

replace surjectivity with right-inverse

eric-wieser committed 2 years ago

79eb5555

eric-wieser committed 2 years ago

0955d063

revert a golf that no longer works

eric-wieser committed 2 years ago

64a52c6c

eric-wieser committed 2 years ago

d805008d

apply suggested golf

eric-wieser committed 2 years ago

5c230f5f

Merge remote-tracking branch 'origin/master' into Dihedral-Group-Lemmas

eric-wieser committed 2 years ago

fdb92dd2

feat(group_theory/monoid_localization): Order (#18724)

YaelDillies committed 2 years ago

13b8e258

chore(order/initial_seg): tweak `subsingleton_of_trichotomous_of_irrefl` (#18749)

vihdzp committed 2 years ago

730c6d4c

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

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

Older