leanprover-community/mathlib3

Pull Requests Commits

feat(category_theory/yoneda): add iso_comp_punit (#5448)

kbuzzard committed 5 years ago

c5c02ec8

feat(category_theory/limits): yoneda preserves limits (#5439)

b-mehta committed 5 years ago

c98d5bb0

chore(category_theory/sites/sheaf): rename sheaf to sheaf_of_types (#5458)

kbuzzard committed 5 years ago

4778e165

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

leanprover-community-bot committed 5 years ago

ca2e536f

feat(tactic/field_simp): let field_simp use norm_num to prove numerals are nonzero (#5418)

sgouezel committed 5 years ago

d79105ef

feat(topology/algebra/ordered): continuity of `abs` (#5412)

urkud committed 5 years ago

50107383

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

leanprover-community-bot committed 5 years ago

a9fb069b

feat(field_theory/galois): Separable splitting field is Galois (#5347)

tb65536 committed 5 years ago

1cb97275

chore(data/nat/cast,algebra/ordered_group): 2 trivial lemmas (#5436)

urkud committed 5 years ago

e22fb94e

chore(algebra/ordered_group): deduplicate (#5403)

urkud committed 5 years ago

5de67573

feat(topology/algebra/ordered): a linear ordered additive group with order topology is a topological group (#5402)

urkud committed 5 years ago

63e7fc96

feat(measure_theory/lp_space): add lemmas about the monotonicity of the Lp seminorm (#5395)

RemyDegenne committed 5 years ago

154a0242

feat(ring_theory/roots_of_unity): lemmas about minimal polynomial (#5393)

riccardobrasca committed 5 years ago

ce385a05

chore(analysis/calculus/{fderiv,deriv}): `f x ≠ f a` for `x ≈ a`, `x ≠ a` if `∥z∥ ≤ C * ∥f' z∥` (#5420)

urkud committed 5 years ago

c55721d6

feat(ring_theory/witt_vector): redefine subtraction using witt_sub polynomial (#5405)

jcommelin committed 5 years ago

ff830d7e

feat(category_theory): essential image of a functor (#5352)

b-mehta committed 5 years ago

656b1bb5

chore(ring_theory/power_series): review, golf (#5431)

urkud committed 5 years ago

0bb665cc

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

leanprover-community-bot committed 5 years ago

53354e7d

chore(linear_algebra/multilinear): Add map_update_zero (#5417)

eric-wieser committed 5 years ago

ec1b70eb

feat(data/fin): trans and id lemmas for fin.cast (#5415)

pechersky committed 5 years ago

5e057c94

feat(data/nat/basic): succ_lt_succ_iff (#5422)

pechersky committed 5 years ago

0e9a77cc

chore(analysis/special_functions/trigonometric): golf a few more proofs (#5423)

urkud committed 5 years ago

33483a3d

feat(data/set/basic): nonempty instances for subtypes (#5409)

hrmacbeth committed 5 years ago

0d140b15

feat(linear_algebra/tensor_product): Inherit smul through is_scalar_tower (#5317)

eric-wieser committed 5 years ago

775edc61

chore(topology/algebra/ordered): generalize `tendsto_at_top_add_left` etc (#5398)

urkud committed 5 years ago

74b58397

chore(analysis/normed_space/basic): `continuous_at.norm` etc (#5411)

urkud committed 5 years ago

c4f673cb

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

leanprover-community-bot committed 5 years ago

a4dd9e18

chore(analysis/special_functions/trigonometric): review, golf (#5392)

urkud committed 5 years ago

b1218f8b

chore(algebra/module/basic): add `subsingleton (semimodule ℕ M)` (#5396)

eric-wieser committed 5 years ago

35f2789c

chore(algebra/{group,ring}): more on pushing/pulling groups/rings along morphisms (#5406)

jcommelin committed 5 years ago

6f1351f3

Newer Older