leanprover-community/mathlib

Pull Requests Commits

feat(data/nat/factorial): descending factorial (#7759)

YaelDillies committed 4 years ago

f8e9c179

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

b-mehta committed 4 years ago

2dcc307e

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

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

chore(field_theory): turn `intermediate_field.subalgebra.equiv_of_eq` into `intermediate_field.equiv_of_eq` (#8069)

Vierkantor committed 4 years ago

25d8aac6

feat(data/polynomial): `aeval_alg_equiv`, like `aeval_alg_hom` (#8038)

Vierkantor committed 4 years ago

db84f2b6

chore(data/polynomial): generalize `aeval_eq_sum_range` to `comm_semiring` (#8037)

Vierkantor committed 4 years ago

2a155208

docs(data/list/pairwise): add module docstring (#8025)

YaelDillies committed 4 years ago

3937c1b2

feat(analysis/convex/exposed): introduce exposed sets (#7928)

YaelDillies committed 4 years ago

520e79d9

feat(measure_theory): the Vitali-Caratheodory theorem (#7766)

sgouezel committed 4 years ago

4801fa66

chore(linear_algebra): switch to named constructors for linear_map (#8059)

eric-wieser committed 4 years ago

b9bf921c

chore(data/polynomial/eval, ring_theory/polynomial_algebra): golfs (#8058)

eric-wieser committed 4 years ago

2a1cabea

feat(data/matrix/basic.lean) : added map_scalar and linear_map.map_matrix (#8061)

faenuccio committed 4 years ago

5352639d

feat(analysis/liouville/liouville_constant): transcendental Liouville numbers exist! (#8020)

adomani committed 4 years ago

5bd649fb

Newer Older