leanprover-community/mathlib

Pull Requests Commits

erdOne committed 3 years ago

14f1e8f9

Merge branch 'master' of https://github.com/leanprover-community/mathlib into kaehler_differential_exact_seq

erdOne committed 3 years ago

45cf530c

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

feat(order/succ_pred/linear_locally_finite): there is an order_iso between a linear locally finite order and a subset of Z (#16832)

RemyDegenne committed 3 years ago

2647cabe

feat(algebraic_topology/dold_kan): a few basic lemmas and a property of P_infty (#17538)

joelriou committed 3 years ago

ed98c07f

chore(data/rat/defs): remove unneeded import (#17532)

kim-em committed 3 years ago

ec5a68fa

refactor(algebra/ring/basic): postpone an import (#17531)

kim-em committed 3 years ago

fefc4e05

refactor(algebra/*): streamlining up to data.nat.cast.basic (#17530)

kim-em committed 3 years ago

2fc6f911

feat(geometry/manifold/mfderiv): add arithmetic lemmas (#17432)

CBirkbeck committed 3 years ago

0616cee2

feat(ring_theory/ideal/operations): the Third Isomorphism theorem for rings (#17243)

Paul-Lez committed 3 years ago

ba169ae3

feat(data/list/{basic,join}): towards `take_join` (#17190)

madvorak committed 3 years ago

0f06bccf

refactor(topology/algebra/module/basic): don't import determinant (#17517)

kim-em committed 3 years ago

4b262b84

chore(data/rat/init): freeze (#17529)

mcdoll committed 3 years ago

aab56fd7

Older