leanprover-community/mathlib

Pull Requests Commits

chore(group_theory/perm/sign): remove classical for sign congr simp lemmas (#5622)

pechersky committed 5 years ago

47c60812

chore(group_theory/perm/basic): Add some missing simp lemmas (#5614)

eric-wieser committed 5 years ago

9dd1496a

feat(algebra/subalgebra): Restrict injective algebra homomorphism to algebra isomorphism (#5560)

tb65536 committed 5 years ago

24572870

feat(algebra/algebra/ordered): ordered algebras (#4683)

kim-em committed 5 years ago

2c8175fa

chore(docs/100.yaml): Freek No. 15 (#5638)

benjamindavidson committed 5 years ago

95c70870

refactor(analysis/special_functions/trigonometric): redefine arcsin and arctan (#5300)

urkud committed 5 years ago

a32e2236

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

leanprover-community-bot committed 5 years ago

3f359612

feat(data/list/zip): parameterize zip_append more generally (#5650)

cemulate committed 5 years ago

f668be05

chore(ring_theory/ideal/basic): Make an argument to mul_mem_{left,right} explicit (#5611)

eric-wieser committed 5 years ago

f4128dc4

feat(linear_algebra/tensor_product,algebra/module/linear_map): Made tmul_smul and map_smul_of_tower work for int over semirings (#5430)

eric-wieser committed 5 years ago

91fcb480

feat(analysis/normed_space/inner_product): facts about the span of a single vector, mostly in inner product spaces (#5589)

hrmacbeth committed 5 years ago

eeb194dc

feat(ring_theory/finiteness): add finitely presented algebra (#5407)

riccardobrasca committed 5 years ago

186ad763

feat(ring_theory/fractional_ideal): move inv to dedekind_domain (#5053)

faenuccio committed 5 years ago

35ff0434

feat(computability/regular_expressions): define regular expressions (#5036)

foxthomson committed 5 years ago

1db70a89

feat(tactic/rewrite_search): Automatically searching for chains of rewrites (#4841)

lacker committed 5 years ago

137a6e0f

feat(category_theory/monad): generalise limits lemma (#5630)

b-mehta committed 5 years ago

062f2443

feat(category_theory/adjunction): mates (#5599)

b-mehta committed 5 years ago

56ed5d78

feat(group_theory): add definition of solvable group (#5565)

pglutz committed 5 years ago

5f98a961

feat(algebra/lie/basic): the lattice of Lie submodules of a Noetherian Lie module is well-founded (#5557)

Oliver Nash committed 5 years ago

648ff216

fix(algebra/group/pi): use correct `div`/`sub` (#5625)

urkud committed 5 years ago

38921554

feat(data/list/chain): chain pmap (#5438)

b-mehta committed 5 years ago

3d6ba9a7

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

leanprover-community-bot committed 5 years ago

de739122

feat(order/atoms): Pairwise coprime (#5596)

tb65536 committed 5 years ago

19d2ea76

feat(linear_algebra/affine_space/midpoint): a few more lemmas (#5571)

urkud committed 5 years ago

9fdd703b

refactor(*): swap sides of `iff` in `{rel_embedding,order_embedding}.map_rel_iff` (#5556)

urkud committed 5 years ago

731c26f2

chore(measure_theory/pi): a few more lemmas (#5604)

urkud committed 5 years ago

8f424fca

feat(analysis/normed_space/inner_product): inner product is continuous, norm squared is smooth (#5600)

urkud committed 5 years ago

00d86176

fix(algebra/group/prod): fixes for #5563 (#5577)

urkud committed 5 years ago

0c8fffe9

feat(analysis/normed_space/inner_product): consequences of characterization of orthogonal projection (#5558)

hrmacbeth committed 5 years ago

7cf0a29d

feat(ring_theory/roots_of_unity): degree of minimal polynomial (#5475)

riccardobrasca committed 5 years ago

82ec0ccb

Newer Older