leanprover-community/mathlib

Pull Requests Commits

jcommelin committed 3 years ago

0f9c036e

Lint says that these are not good instances

nomeata committed 3 years ago

f894082d

Review feedback

nomeata committed 3 years ago

066d12e9

feat(group_theory/sylow): add characteristic_of_normal

nomeata committed 3 years ago

2234ee3c

feat(number_theory/cyclotomic/basic): add missing lemmas (#11451)

riccardobrasca committed 3 years ago

b1ad3012

chore(analysis/normed/group/completion): fix attribution (#11614)

hrmacbeth committed 3 years ago

9a517cf0

chore(data/complex/is_R_or_C): squeeze simps (#11251)

dupuisf committed 3 years ago

2babfeb0

feat(measure_theory/covering): Lebesgue density points (#11554)

sgouezel committed 3 years ago

84dbe7ba

chore(measure_theory/probability_mass_function): Move pmf monad operations into a seperate file (#11579)

dtumad committed 3 years ago

a196f9be

feat(topology/instances/ennreal): continuity of subtraction on ennreal (#11527)

sgouezel committed 3 years ago

31db25b4

split(order/max): Split off `order.basic` (#11603)

YaelDillies committed 3 years ago

159d9aca

feat(topology): add a few lemmas (#11607)

urkud committed 3 years ago

5080d64d

move(order/hom/order): Move from `order.hom.lattice` (#11601)

YaelDillies committed 3 years ago

bd3b892f

doc(group_theory.quotient_group): Fix typos in main statement list (#11581)

nomeata committed 3 years ago

206b56ec

feat(group_theory/abelianization): add mul_equiv.abelianization_congr (#11466)

nomeata committed 3 years ago

155cf1df

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

Older