leanprover-community/mathlib3

Pull Requests Commits

feat(group_theory/schreier): A theorem of Schur: A group with finitely many commutators has finite commutator subgroup (#17311)

tb65536 committed 3 years ago

91ce9cbd

chore: freeze logic.relation (#17573)

kbuzzard committed 3 years ago

71dbd401

feat(algebra/ne_zero): generalize lemmas (#17477)

astrainfinita committed 3 years ago

bb168510

refactor(*): scrub imports (#17568)

kim-em committed 3 years ago

70fd9563

fix(tactic/choose): typo (#17552)

fzyzcjy committed 3 years ago

fd47bdf0

feat(ring_theory/polynomial/cyclotomic): generalize some lemmas to `[ring R]` (#17555)

urkud committed 3 years ago

83490903

feat(data/list/join): add `list.append_join_append` and `list.reverse_join` (#17554)

madvorak committed 3 years ago

c34a1aa4

chore(*): golf (#17558)

urkud committed 3 years ago

17a9f8f7

chore(*): add mathlib4 synchronization labels (#17556)

j-loreaux committed 3 years ago

7cca1710

chore(topology/algebra/order/basic): move field-parts into new file (#17549)

mcdoll committed 3 years ago

49ae0e37

feat(data/set/prod): Preimage of `set.pi` (#17534)

YaelDillies committed 3 years ago

1955c1cf

fix(tactic/linarith): fix bug in linarith (#17307)

kim-em committed 3 years ago

693ae04f

chore(algebra/group/defs): fix to_additive instance name (#17079)

kim-em committed 3 years ago

bfe9e712

refactor(topology/{fiber,vector}_bundle): make `vector_bundle` a mixin (#17505)

hrmacbeth committed 3 years ago

b8c810e2

chore(linear_algebra): import `free_module.finite.rank` from `finite_dimensional` (#17482)

Vierkantor committed 3 years ago

bf2a9e01

feat(analysis/calculus/local_extr): generalize `polynomial.card_root_set_le_derivative` (#17315)

urkud committed 3 years ago

fc7dbc95

chore(algebra/algebra): reduce imports for `algebra.algebra.tower` (#17476)

Vierkantor committed 3 years ago

a35ddf20

feat(analysis/normed/order/basic): Non-linear normed ordered groups (#17238)

YaelDillies committed 3 years ago

f3603f07

feat(data/(d)finsupp,fintype,fun_like): add fintype and (in)finite instances (#15725)

alexjbest committed 3 years ago

3cd7b577

fix(tactic/assert_exists): avoid name collisions in linter declarations (#17550)

eric-wieser committed 3 years ago

8c53048a

feat(combinatorics/simple_graph/prod): add finset lemma and remove unecessary `decidable_eq` (#17461)

eric-wieser committed 3 years ago

2985fa3c

feat(ring_theory/ideal): define `submodule.card_quot` (#17102)

Vierkantor committed 3 years ago

cc165837

feat(group_theory/group_action/quotient): If `G=<S>`, then `G / Z(G)` embeds into `S → {[g₁, g₂]}` (#17151)

tb65536 committed 3 years ago

5e4b2d4a

feat(ring_theory/derivation): A presentation of the Kähler differential module (#17011)

erdOne committed 3 years ago

b40c1406

chore(ring_theory/roots_of_unity): golf some proofs (#17546)

urkud committed 3 years ago

6075e179

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

leanprover-community-bot committed 3 years ago

9c759b4c

feat(group_theory/free_group): to_additivize where possible (#17034)

alexjbest committed 3 years ago

a22318f3

feat(algebra/module/pi): Non-dependent shortcut (#17536)

YaelDillies committed 3 years ago

2c28ce03

feat(linear_algebra/affine_space/affine_subspace): `mem_mk'_iff_vsub_mem` (#17524)

jsm28 committed 3 years ago

93f2a636

feat(logic/equiv/basic): `coe_prod_comm` (#17510)

YaelDillies committed 3 years ago

d5d94ecd

Newer Older