leanprover-community/mathlib3

Pull Requests Commits

Merge branch 'master' into bundle-cont-bilinear

urkud committed 4 years ago

70011a86

feat(category_theory/is_connected): constant functor is full (#8233)

b-mehta committed 4 years ago

aa78feba

chore(analysis/normed_space/banach): speed up the proof (#8230)

eric-wieser committed 4 years ago

b1806d19

feat(topology/algebra/infinite_sum): summable_empty (#8241)

gihanmarasingha committed 4 years ago

9e0462c0

feat(category_theory/limits): transfer limit creation along diagram iso (#8237)

b-mehta committed 4 years ago

e18b3a89

feat(linear_algebra/matrix/nonsingular_inverse): more lemmas (#8216)

l534zhan committed 4 years ago

d0e09dde

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

leanprover-community-bot committed 4 years ago

b52c1f0c

feat(category_theory/category/Kleisli): Fix lint errors (#8244)

b-mehta committed 4 years ago

70320f74

feat(measure_theory/borel_space): a preconnected set is measurable (#8044)

ADedecker committed 4 years ago

a444e81f

feat(algebra/category): provide right adjoint instances for forget (#8235)

b-mehta committed 4 years ago

bcd61b1d

chore(data/set/basic): use `decidable_pred (∈ s)` instead of `decidable_pred s`. (#8211)

eric-wieser committed 4 years ago

ee018175

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

Nicknamen committed 4 years ago

a312e7e2

feat(analysis/complex/isometry): restate result more abstractly (#7908)

hrmacbeth committed 4 years ago

abde2102

feat(category_theory/limits): finite products from finite limits (#8236)

b-mehta committed 4 years ago

11348653

feat(measure_theory/measure_space): prob_le_one (#7913)

hmonroe committed 4 years ago

e46447be

feat(group_theory,linear_algebra): third isomorphism theorem for groups and modules (#8203)

Vierkantor committed 4 years ago

9d40a598

feat(linear_algebra/prod): add coprod_map_prod (#8220)

eric-wieser committed 4 years ago

a7b660e4

chore(measure_theory/measure_space): untangle `probability_measure`, `finite_measure`, and `has_no_atoms` (#8222)

eric-wieser committed 4 years ago

13486fe5

feat(data/finset/noncomm_prod): noncomm_prod_union_of_disjoint (#8169)

pechersky committed 4 years ago

b10062e7

feat(data/nat/basic): lt_one_iff (#8224)

pechersky committed 4 years ago

a4b0b48b

refactor(order/rel_iso): move statements about intervals to data/set/intervals (#8150)

eric-wieser committed 4 years ago

fb22ae33

chore(group_theory/perm/support): support_pow_le over nat (#8225)

pechersky committed 4 years ago

03e2cbd0

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

leanprover-community-bot committed 4 years ago

0ee238cf

feat(group_theory/perm/list): concrete permutations from a list (#7451)

pechersky committed 4 years ago

70aef28e

fix(data/complex/basic): ensure `algebra ℝ ℂ` is computable (#8166)

eric-wieser committed 4 years ago

5f2358c4

feat(algebra/group/units): teach `simps` about `units` (#8204)

eric-wieser committed 4 years ago

e0ca8534

fix(data/real/basic): provide a computable `module` instance (#8164)

eric-wieser committed 4 years ago

ce3d53b0

chore(feat/algebra/lie/from_cartan_matrix): rename file (#8219)

ocfnash committed 4 years ago

05e8ed24

docs(category_theory/limits/shapes/products): add module docstring (#8212)

b-mehta committed 4 years ago

836c5491

feat(data/fintype/list): induced fintype on nodup lists (#8171)

pechersky committed 4 years ago

51452619

Older