leanprover-community/mathlib3

Pull Requests Commits

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

chore(order/bounds): golf (#5401)

urkud committed 5 years ago

ff716d24

chore(topology/algebra/ordered): deduplicate (#5399)

urkud committed 5 years ago

3685146a

feat(algebra/module/basic): Add symmetric smul_comm_class instances for int and nat (#5369)

eric-wieser committed 5 years ago

35a16a94

chore(linear_algebra/{alternating,multilinear}): Add a handful of trivial lemmas (#5380)

eric-wieser committed 5 years ago

ee6969c3

chore(analysis/calculus/deriv): add `iff` versions of `differentiable_const_add` etc (#5390)

urkud committed 5 years ago

6a99e9e8

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

leanprover-community-bot committed 5 years ago

e8fc373a

chore(analysis/analytic/basic.lean): fix latex in doc (#5397)

sgouezel committed 5 years ago

01a77adc

feat(ring_theory/algebra_tower): alg_hom_equiv_sigma (#5345)

tb65536 committed 5 years ago

8fa10afc

chore(script/copy-mod-doc) Specify an encoding for files when opening (#5394)

alexjbest committed 5 years ago

c5a2ff4c

feat(finset): two simple lemmas (#5387)

fpvandoorn committed 5 years ago

9282f6cd

chore(group_theory/group_action/basic): Add a simp lemma about smul on quotient groups (#5374)

eric-wieser committed 5 years ago

39ecd1ab

chore(*): add a `div`/`sub` field to (`add_`)`group`(`_with_zero`) (#5303)

Vierkantor committed 5 years ago

1221ab6b

Newer Older