leanprover-community/mathlib3

Pull Requests Commits

erdOne committed 3 years ago

bafddfb6

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

refactor(algebra/order/ring): Make `strict_ordered_semiring`s nontrivial (#17394)

YaelDillies committed 3 years ago

53b216bc

feat(scripts/modules_used): list imported modules which are actually used (#17507)

kim-em committed 3 years ago

36f5ed00

chore(ring_theory): split finiteness into finite, finite type and finite presentation (#17481)

Vierkantor committed 3 years ago

6e7ca692

feat(ring_theory): induction and multiplicativity via prime factorization (#17192)

Vierkantor committed 3 years ago

597343b0

feat(linear_algebra/free_module): lemmas on ideal quotient of a free module over a PID (#17103)

Vierkantor committed 3 years ago

b8e1f0f7

feat(tactic/positivity): Extension for natural powers in a `canonically_ordered_comm_semiring` (#17535)

YaelDillies committed 3 years ago

1158f6d8

feat(tactic/assert_exists): add a linter to protect against typos (#17519)

eric-wieser committed 3 years ago

159e1e20

Older