leanprover-community/mathlib3

Pull Requests Commits

feat(linear_algebra/affine_space/finite_dimensional): more lemmas (#4389)

jsm28 committed 5 years ago

1c8bb422

feat(number_theory/arithmetic_function): Define arithmetic functions/the Dirichlet ring (#4352)

awainverse committed 5 years ago

565e961d

feat(category_theory/limits/terminal): limit of a diagram with initial object (#4404)

b-mehta committed 5 years ago

9ab7f055

chore(algebra/ring/basic): docs, simps (#4375)

urkud committed 5 years ago

91d9e963

feat(analysis/complex/roots_of_unity): complex (primitive) roots of unity (#4330)

jcommelin committed 5 years ago

08cdf37c

feat(category_theory/limits): lift self limit (#4403)

b-mehta committed 5 years ago

bf998892

feat(topology): completion of separable space is separable (#4399)

PatrickMassot committed 5 years ago

916b5d3a

feat(analysis/special_functions/pow): exp_mul (#4409)

jsm28 committed 5 years ago

fc09dbae

feat(algebra/big_operators/order): bounding finite fibration cardinalities from below (#4396)

Oliver Nash committed 5 years ago

d13d21ba

feat(linear_algebra/dimension): one-dimensional spaces (#4400)

jsm28 committed 5 years ago

f437365a

feat(data/nat): Slightly strengthen nat.coprime_of_dvd/nat.coprime_of_dvd' (#4368)

Ruben-VandeVelde committed 5 years ago

8f536768

feat(data/set/basic): subsingleton_coe (#4388)

jsm28 committed 5 years ago

729b60a2

feat(data/set/basic): eq_singleton_iff_unique_mem (#4387)

jsm28 committed 5 years ago

e8b65e68

feat(algebra/group): construct `add_monoid_hom` from `map_sub` (#4382)

urkud committed 5 years ago

e1b1d17a

chore(data/equiv/mul_add): add more `equiv` lemmas to `mul_equiv` namespace (#4380)

urkud committed 5 years ago

231271d3

feat(algebra/gcd_monoid, data/*set/gcd): a few lemmas about gcds (#4354)

awainverse committed 5 years ago

5d35b9ad

feat(linear_algebra/basic): span_singleton smul lemmas (#4394)

jsm28 committed 5 years ago

509dd9ea

chore(data/mv_polynomial): rename `pderivative` to `pderiv` (#4381)

urkud committed 5 years ago

c3d08357

feat(category_theory/limits/cofinal): better API for cofinal functors (#4276)

kim-em committed 5 years ago

e902cae5

feat(algebra/group_power/identities): named ring identities (#4390)

bryangingechen committed 5 years ago

e738e905

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

leanprover-community-bot committed 5 years ago

f2044a57

chore(algebra/group/type_tags): Use ≃ instead of → (#4346)

eric-wieser committed 5 years ago

333c2164

doc(data/real/*): add a few docstrings, `ereal.has_zero`, and `ereal.inhabited` (#4378)

urkud committed 5 years ago

a0ba5e7d

feat(algebra/ordered*): more simp lemmas (#4359)

urkud committed 5 years ago

e593ffa6

feat(slim_check): sampleable instance for generating functions and injective functions (#3967)

cipher1024 committed 5 years ago

b790b27d

doc(*): add a few short module docstrings (#4370)

urkud committed 5 years ago

c39170e4

chore(.github/workflows): github action for crossing off PR dependencies (#4367)

bryangingechen committed 5 years ago

946ab026

chore(category_theory/limits/binary_products): weaken assumptions (#4373)

b-mehta committed 5 years ago

069952b8

feat(data/monoid_algebra): Allow R ≠ k in semimodule R (monoid_algebra k G) (#4365)

eric-wieser committed 5 years ago

9e455c15

chore(category_theory/limits/equalizers): some equalizer fixups (#4372)

b-mehta committed 5 years ago

6ab3eb7c

Newer Older