Commits leanprover-community/mathlib

fix(category_theory/triangulated): Fix definition of pretriangulated (#11596)

erdOne committed 3 years ago

7ba08d3c

chore(group_theory/nilpotent): golf some proofs (#11599)

Ruben-VandeVelde committed 3 years ago

d1b51655

chore(analysis/normed_space/star): golf some lemmas (#11600)

Ruben-VandeVelde committed 3 years ago

fbf3c643

feat(group_theory.nilpotent): add *_central_series_one G 1 = … simp lemmas (#11584)

nomeata committed 3 years ago

504e1f60

feat(order/antichain): Strong antichains (#11400)

YaelDillies committed 3 years ago

b630b8cd

feat(algebra/algebra/operations): remove two hypotheses from `submodule.mul_induction_on` (#11533)

eric-wieser committed 3 years ago

0ca77959

feat(group_theory/subgroup/basic): add center_le_normalizer (#11590)

nomeata committed 3 years ago

5e9c0a56

chore(analysis/normed/group/basic): merge `norm` and `semi_norm` lemmas on `prod` and `pi` (#11492)

eric-wieser committed 3 years ago

d99f2fd7

chore(category_theory/sites): Generalize universes for the comparison lemma. (#11588)

erdOne committed 3 years ago

0653975e

feat(analysis/fourier): Fourier series for functions in L2; Parseval's identity (#11320)

hrmacbeth committed 3 years ago

049d2aca

refactor(src/order/bounded): Invert iff direction (#11582)

vihdzp committed 3 years ago

9c39019f

feat(order/bounded): Proved many lemmas about bounded and unbounded sets (#11179)

vihdzp committed 3 years ago

ca795135

chore(analysis/inner_product_space/dual): remove unneeded `complete_space` assumption in four lemmas (#11578)

dupuisf committed 3 years ago

884d8137

feat(data/finset/basic): random golf (#11576)

ericrbg committed 3 years ago

80e072ec

feat(analysis/seminorm): add composition with linear maps (#11477)

mcdoll committed 3 years ago

d71cab9f

feat(group_theory/submonoid/pointwise): add pointwise multiplication to `add_submonoid`s (#11522)

eric-wieser committed 3 years ago

6c97821d

feat(measure_theory/function/lp_space): some variations of Markov's inequality formulated using `snorm` (#11478)

kex-y committed 3 years ago

adadd4af

chore(*): Remove tactic.unfreeze_local_instances (#11507)

huynhtrankhanh committed 3 years ago

8c9074f8

feat(data/sym/sym2): add lemma that eq from distinct common members (#11563)

vbeffara committed 3 years ago

dfca2b0f

feat(group_theory/nilpotent): Add equality theorems for nilpotency class (#11540)

nomeata committed 3 years ago

b87449ab

feat(measure_theory/measurable_space): defining a measurable function on countably many pieces (#11532)

sgouezel committed 3 years ago

b5e542d3

feat(ring_theory/{norm.lean, trace.lean}): improve two statements. (#11569)

riccardobrasca committed 3 years ago

1d762c7e

feat(topology/uniform_space/uniform_convergence): Composition on the left (#11560)

tb65536 committed 3 years ago

447928c9

feat(analysis/inner_product_space/l2): a Hilbert space is isometrically isomorphic to `ℓ²` (#11255)

hrmacbeth committed 3 years ago

5a40c33f

feat(*): lemmas about `disjoint` on `set`s and `filter`s (#11549)

urkud committed 3 years ago

53650a00

feat(analysis/normed_space/finite_dimension): extending partially defined Lipschitz functions (#11530)

sgouezel committed 3 years ago

e96e55d8

chore(topology/uniform_space/uniform_convergence): Golf some proofs (#11561)

tb65536 committed 3 years ago

0a8848ac

doc(group_theory/free_group): fix linkify (#11565)

ericrbg committed 3 years ago

656372c4

chore(*): to_additive related cleanup (#11559)

alexjbest committed 3 years ago

0bb42725

feat(data/finsupp/basic): lemmas about map domain with only inj_on hypotheses (#11484)

alexjbest committed 3 years ago

7ee41aab