leanprover-community/mathlib

Pull Requests Commits

Merge branch 'counting-measure' of github.com:leanprover-community/mathlib into counting-measure

kckennylau committed 6 years ago

a32a8f2f

change ite to if-then-else

kckennylau committed 6 years ago

e1612934

Merge branch 'master' into counting-measure

kckennylau committed 6 years ago

Verified 6420db23

feat(measure_theory/counting_measure): counting measure

kckennylau committed 6 years ago

85d43fc4

feat(group_theory/conjugates) : define conjugates (#1029)

Michael-Howes committed 6 years ago

d4343972

refactor(set_theory/ordinal): shorten proof of well_ordering_thm (#1078)

ChrisHughes24 committed 6 years ago

c6a7f300

chore(CommRing/adjunctions): refactor proofs (#1049)

kim-em committed 6 years ago

62acd6b8

doc(finsupp,category_theory): fixes (#1075)

fpvandoorn committed 6 years ago

15fecbdd

feat(linear_algebra/basic): general_linear_group basics (#1064)

jcommelin committed 6 years ago

d07e3b3e

feat(data/nat): various lemmas (#1017)

kim-em committed 6 years ago

f004d327

feat(*): image_closure (#1069)

jcommelin committed 6 years ago

971ddcc2

refactor(integration.lean): changing `measure_space` to `measurable_space` (#1072)

kodyvajjha committed 6 years ago

34613996

feat(algebra/pi_instances): product of submonoids/groups/rings (#1066)

jcommelin committed 6 years ago

cb30c97e

feat(category_theory): limits in CommRing (#1006)

kim-em committed 6 years ago

0ab8a89d

chore(topology/algebra/monoid): continuous_mul_left/right (#1065)

jcommelin committed 6 years ago

8cf7c4c8

chore(ring_theory/algebra): simp-lemmas for alg_hom.to_linear_map (#1062)

jcommelin committed 6 years ago

593938cd

feat(tactic/basic): adds `contrapose` tactic (#1015)

PatrickMassot committed 6 years ago

d001abfd

feat(topology/opens): continuous.comap : opens Y → opens X (#1061)

jcommelin committed 6 years ago

15a6af22

feat(tactic/linarith): better input syntax linarith only [...] (#1056)

robertylewis committed 6 years ago

d4c7b7a6

refactor: coherent composition order (#1055)

sgouezel committed 6 years ago

f2534017

refactor(topology/metric/gromov_hausdorff): make Hausdorff_edist irreducible (#1052)

sgouezel committed 6 years ago

cb4c9ee7

feat(topology/order): make nhds irreducible (#1043)

robertylewis committed 6 years ago

b9cb69c3

feat(tactic/squeeze): remove noise from output (#1047)

cipher1024 committed 6 years ago

Verified 73c3f717

refactor(data/complex/exponential): improve trig proofs (#1041)

digama0 committed 6 years ago

fa0e7570

feat(adjointify): make definition easier for elaborator (#1045)

fpvandoorn committed 6 years ago

5e5298b9

fix(topology/stone_cech): faster proof from @PatrickMassot (#1042)

rwbarton committed 6 years ago

45afa86e

feat(set_theory/surreal): surreal numbers (#958)

digama0 committed 6 years ago

901178e2

refactor: change variables order in some composition lemmas (#1035)

sgouezel committed 6 years ago

0b350228

feat(tactic/basic): add tactic.rewrite, and sort list (#1039)

jcommelin committed 6 years ago

f633c948

fix(data/complex/exponential): make complex.exp irreducible (#1040)

robertylewis committed 6 years ago

a6c1f377

Older