leanprover-community/mathlib3

Pull Requests Commits

b-mehta committed 4 years ago

Verified 36592cd7

review suggestion

b-mehta committed 4 years ago

Verified 66ff800b

review suggestion

b-mehta committed 4 years ago

Verified b58c724c

Merge branch 'master' into strict-initial

b-mehta committed 4 years ago

Verified 097c833c

Merge branch 'master' into strict-initial

b-mehta committed 4 years ago

Verified b6bc2622

b-mehta committed 4 years ago

Verified 352c26ff

feat(category_theory/limits): morphism to terminal is split mono (#8084)

b-mehta committed 4 years ago

2dcc307e

strict initials

b-mehta committed 4 years ago

Verified b8d76e55

Merge branch 'split-mono-terminal' into strict-initial

b-mehta committed 4 years ago

Verified fbe5f585

review suggestions

b-mehta committed 4 years ago

Verified 174b035d

chore(scripts): update nolints.txt (#8093)

leanprover-community-bot committed 4 years ago

c5d17ae1

doc(topology/homeomorph): fixup glaring error (#8092)

ericrbg committed 4 years ago

c7a35b41

doc(topology/homeomorph): module docs (#8086)

ericrbg committed 4 years ago

0817020b

feat(field_theory): state primitive element theorem using `power_basis` (#8073)

Vierkantor committed 4 years ago

b874abc7

feat(algebraic_topology/simplicial_object): Add augment construction (#8085)

adamtopaz committed 4 years ago

598722a2

chore(data/set/intervals): syntax clean up (#8087)

YaelDillies committed 4 years ago

4630067c

chore(analysis/analytic/composition): remove one `have` (#8083)

adomani committed 4 years ago

68ec06cf

feat(measure_theory/interval_integral): generalize `add_adjacent_intervals` to n-ary sum (#8050)

ADedecker committed 4 years ago

92a71712

fix(real/sign): make `real.sign 0 = 0` to match `int.sign 0` (#8080)

eric-wieser committed 4 years ago

6666ba2f

docs(data/list/chain): add module docstring (#8041)

YaelDillies committed 4 years ago

a7faaf53

docs(data/list/range): add module docstring (#8026)

YaelDillies committed 4 years ago

cf4a2df2

Merge branch 'split-mono-terminal' into strict-initial

b-mehta committed 4 years ago

Verified d5b1adb3

morphism to terminal is split mono

b-mehta committed 4 years ago

Verified 3531839b

feat(ring_theory/nilpotent): basic results about nilpotency in associative rings (#8055)

ocfnash committed 4 years ago

9cc44ba2

chore(data/complex/{module, is_R_or_C}, analysis/complex/basic): rationalize the structure provided for `conj` and `of_real` (#8014)

hrmacbeth committed 4 years ago

1774cf95

feat(ring_theory/power_basis): map a power basis through an alg_equiv (#8039)

Vierkantor committed 4 years ago

c5153466

docs(overview, undergrad): add Liouville's Theorem on existence of transcendental numbers (#8068)

adomani committed 4 years ago

10cd252f

feat(data/matrix/basic): add lemma minor_map (#8074)

faenuccio committed 4 years ago

26082445

chore(algebraic_topology/simplex_category): golf proof (#8076)

kbuzzard committed 4 years ago

e137523a

feat(linear_algebra/pi): add linear_equiv.Pi_congr_left (#8070)

eric-wieser committed 4 years ago

e605b21f

Older