leanprover-community/mathlib

Pull Requests Commits

move more stuff

winston-h-zhang committed 4 years ago

a8b1919b

chore(algebra/algebra/basic): add algebra.right_comm to match left_comm (#8109)

eric-wieser committed 4 years ago

ac156c15

winston-h-zhang committed 4 years ago

fa62ac57

chore(algebra/ordered_group): remove linear_ordered_comm_group.to_comm_group (#7861)

eric-wieser committed 4 years ago

a79df550

feat(data/complex/module): add complex.alg_hom_ext (#8105)

eric-wieser committed 4 years ago

1ffb5be5

chore(topology/topological_fiber_bundle): reorganizing the code (#7989)

Nicknamen committed 4 years ago

b160ac8d

feat(algebra/lie/nilpotent): basic lemmas about nilpotency for Lie subalgebras of associative algebras (#8090)

ocfnash committed 4 years ago

f7c1e5f2

feat(geometry/manifold): `derivation_bundle` (#7708)

Nicknamen committed 4 years ago

81183ea4

fix(algebra/module/linear_map): do not introduce `show` (#8102)

eric-wieser committed 4 years ago

bfd06851

chore(algebra/ordered_monoid_lemmas): change additive name `left.add_nonneg` to `right.add_nonneg` (#8065)

adomani committed 4 years ago

3cb247c3

fix(algebra/group_power): put opposite lemmas in the right namespace (#8100)

eric-wieser committed 4 years ago

80d02347

winston-h-zhang committed 4 years ago

819e36cb

move stuff to right files

winston-h-zhang committed 4 years ago

f6f6e0dd

feat(group_theory/subgroup): lemmas for normal subgroups of subgroups (#7271)

winston-h-zhang committed 4 years ago

7b253dd5

dont remember what i did

winston-h-zhang committed 4 years ago

26ad6db8

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

Newer Older