leanprover-community/mathlib

Pull Requests Commits

feat(.): add code of conduct (#3747)

robertylewis committed 5 years ago

4324778f

Port lemmas from exterior_algebra

utensil committed 5 years ago

0408c4eb

feat(field_theory/algebraic_closure): algebraic closure (#3733)

kckennylau committed 5 years ago

eb4b2a05

utensil committed 5 years ago

44a7f2a4

Initial setup for Clifford algebra

utensil committed 5 years ago

1f0b8af0

feat(topology/opens): open_embedding_of_le (#3597)

kim-em committed 5 years ago

bfcf6400

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

utensil committed 5 years ago

50a2e510

chore(linear_algebra/exterior_algebra): made proof of wedge_add_swap_adj look nicer

zhangir-azerbayev committed 5 years ago

deb64432

docs(category/default): Fix typo for monomorphism (#3741)

utensil committed 5 years ago

06e14052

refactor(algebra/divisibility, associated): generalize instances in divisibility, associated (#3714)

awainverse committed 5 years ago

f92fd0d1

feat(haar_measure): define the Haar measure (#3542)

fpvandoorn committed 5 years ago

57df7f5a

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

leanprover-community-bot committed 5 years ago

43ceb3e0

chore(algebra/ordered_field): cleanup (#3723)

urkud committed 5 years ago

9e039956

feat(group_theory/group_action): generalize `is_algebra_tower` (#3717)

Vierkantor committed 5 years ago

4a75df92

feat(tactic): fix two bugs with generalize' (#3710)

fpvandoorn committed 5 years ago

37e97b53

Fix units_action

adamtopaz committed 5 years ago

1fa08ffb

Move units action

adamtopaz committed 5 years ago

ec00f609

Add units action

adamtopaz committed 5 years ago

0881beb9

Add ring instance for tensor_algebra

adamtopaz committed 5 years ago

9fbfe5f4

A bit of cleanup

adamtopaz committed 5 years ago

826e7201

feat(category_theory/limits): explicit isomorphisms between preserved limits (#3602)

kim-em committed 5 years ago

47861363

Rewrite \iota, add some lemmas

adamtopaz committed 5 years ago

eec47b5c

chore(category_theory/limits): minor changes in equalizers and products (#3603)

kim-em committed 5 years ago

5680428f

feat(data/list/basic), chore(linear_algebra/tensor_algebra): moved Mario's lemma pmap_map to the correct place. Made some proofs in tensor_algebra look nicer

zhangir-azerbayev committed 5 years ago

478c03f4

feat(linear_algebra/exterior_algebra: proved wedge_perm and necessary lemmas

zhangir-azerbayev committed 5 years ago

40497aac

feat(group_theory/perm/sign: added lemmas necessary to prove wedge_perm

zhangir-azerbayev committed 5 years ago

584f48f3

refactor(linear_algebra/affine_space): split up file (#3726)

jsm28 committed 5 years ago

17ef529d

doc(tactic/lean_core_docs): by_cases is classical (#3718)

lambda-fairy committed 5 years ago

f23fe9a3

chore(linear_algebra/basic): rewrite `p.comap q.subtype` to `comap q.subtype p` (#3725)

Vierkantor committed 5 years ago

d27ddb49

chore(order/complete_lattice): use `order_dual` (#3724)

urkud committed 5 years ago

1675dc40

Newer Older