leanprover-community/mathlib3

Pull Requests Commits

kim-em committed 5 years ago

c943db5a

chore(algebra/group_hom): rename `add_monoid.smul` to `nsmul` (#2861)

urkud committed 5 years ago

a285049b

chore(data/set/basic): add some lemmas to `function.surjective` (#2876)

urkud committed 5 years ago

28e79d48

feat(topology/homeomorph): sum_prod_distrib (#2870)

rwbarton committed 5 years ago

297806e6

feat(tactic/noncomm_ring): add noncomm_ring tactic (#2858)

Oliver Nash committed 5 years ago

0827a30c

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

leanprover-community-bot committed 5 years ago

6e581ef2

chore(order/bounds): +2 lemmas, fix a name (#2877)

urkud committed 5 years ago

c034b4c2

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

leanprover-community-bot committed 5 years ago

9d76ac24

feat(group_theory/group_action): orbit_equiv_quotient_stabilizer_symm_apply and docs (#2864)

kckennylau committed 5 years ago

f05acc8e

refactor(algebra/module): change module into an abbreviation for semimodule (#2848)

urkud committed 5 years ago

67f1951b

feat(algebra/big_operators): prod_ne_zero (#2863)

kckennylau committed 5 years ago

cc06d538

chore(topology): make topological_space fields protected (#2867)

rwbarton committed 5 years ago

b40ac2af

feat(geometry/euclidean): Euclidean space (#2852)

jsm28 committed 5 years ago

62cb7f2f

feat(order/iterate): some inequalities on `f^[n] x` and `g^[n] x` (#2859)

urkud committed 5 years ago

74d446d3

feat(data/equiv): equiv_of_subsingleton_of_subsingleton (#2856)

TwoFX committed 5 years ago

aa47bba5

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

leanprover-community-bot committed 5 years ago

5455fe19

chore(algebra): displace zero_ne_one_class with nonzero and make no_zero_divisors a Prop (#2847)

kckennylau committed 5 years ago

f95e8090

feat(dynamics/fixed_points): define `is_fixed_pt` (#2857)

urkud committed 5 years ago

b2f643e9

feat(tactic/protect_proj): protect_proj attribute for structures (#2855)

ChrisHughes24 committed 5 years ago

836184a8

chore(category_theory): T50000 challenge (#2840)

kim-em committed 5 years ago

77674a04

feat(tactic/with_local_reducibility): alter reducibility attributes locally (#2820)

rwbarton committed 5 years ago

07cdafe9

feat(data/equiv/basic): subtype_prod_equiv_prod (#2717)

rwbarton committed 5 years ago

4a5799e1

feat(ring_theory): define subsemirings (#2837)

urkud committed 5 years ago

b013b2d6

chore(data/setoid): split into `basic` and `partition` (#2853)

urkud committed 5 years ago

6c046c75

feat(analysis/normed_space/add_torsor): normed_add_torsor (#2814)

jsm28 committed 5 years ago

543ae52c

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

leanprover-community-bot committed 5 years ago

e9ba32d1

feat(algebra/free) additive versions, docs. (#2755)

kckennylau committed 5 years ago

ca95726e

refactor(data/equiv/local_equiv): use dot notation for `eq_on_source` (#2830)

urkud committed 5 years ago

cbf4740a

fix(tactic/suggest): normalize synonyms uniformly in goal and lemma (#2829)

Vierkantor committed 5 years ago

28dc2ed5

feat(linear_algebra/lagrange): Lagrange interpolation (#2764)

kckennylau committed 5 years ago

005763ec

Older