leanprover-community/mathlib3

Pull Requests Commits

YaelDillies committed 2 years ago

608a4457

YaelDillies committed 2 years ago

dca0b8b6

actually generalize

YaelDillies committed 2 years ago

Verified 26c10743

generalize normalizer_smul

YaelDillies committed 2 years ago

93d90ba5

YaelDillies committed 2 years ago

b85881ba

YaelDillies committed 2 years ago

0d27e4bf

Merge remote-tracking branch 'origin/master' into conj_subgroup_action

YaelDillies committed 2 years ago

3ac598b8

refactor(algebra/module/dedekind_domain): eliminate existentials (#14734)

eric-wieser committed 2 years ago

cdc34484

feat(data/finset/basic): `insert` and `erase` lemmas (#18729)

YaelDillies committed 2 years ago

9ac7c0c8

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)

github-actions[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)

github-actions[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)

github-actions[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

Older