Commits

Breadcrumbs

History for

onmaster

User selector

All users

All time

Commit history

Commits on Jun 25, 2019

• fix(data/matrix): add brackets to mul_neg and neg_mul to correct statement (#1151)

  Show description for 7484ab4
  

  ChrisHughes24

  authored and

  mergify[bot]

  committed
  7484ab4

  Copy full SHA for 7484ab4

• feat(data/finset): length_sort (#1150)

  

  ChrisHughes24

  authored and

  mergify[bot]

  committed
  a2aeabb

  Copy full SHA for a2aeabb

• feat(algebra/pi_instances): pi.ordered_comm_group (#1152)

  ChrisHughes24

  authored
  c4a4f79

  Copy full SHA for c4a4f79

Commits on Jun 24, 2019

• feat(meta/expr): `simp` and `dsimp` an expr (#1147)

  Show description for c7ee110
  

  khoek

  authored and

  mergify[bot]

  committed
  c7ee110

  Copy full SHA for c7ee110

Commits on Jun 23, 2019

• feat(string): `split_on` a `char` (#1145)

  Show description for d7283d7
  

  khoek

  authored and

  mergify[bot]

  committed
  d7283d7

  Copy full SHA for d7283d7

Commits on Jun 20, 2019

• feat(topology/order): more facts on continuous_on (#1140)

  

  sgouezel

  authored and

  mergify[bot]

  committed
  a35d682

  Copy full SHA for a35d682

Commits on Jun 19, 2019

• chore(topology/*): reverse order on topological and uniform spaces (#1138)

  Show description for e598894
  

  PatrickMassot

  authored and

  mergify[bot]

  committed
  e598894

  Copy full SHA for e598894

• feat(data/set): simple lemmas, renaming (#1137)

  Show description for b1cb48d
  

  sgouezel

  authored and

  mergify[bot]

  committed
  b1cb48d

  Copy full SHA for b1cb48d

Commits on Jun 18, 2019

• fix(category_theory/types): rename lemma `ulift_functor.map` (#1133)

  Show description for 235b899
  

  urkud

  authored and

  mergify[bot]

  committed
  235b899

  Copy full SHA for 235b899

Commits on Jun 17, 2019

• refactor(analysis/normed_space/deriv): split and move to calculus folder (#1135)

  

  sgouezel

  authored and

  mergify[bot]

  committed
  d8d25e9

  Copy full SHA for d8d25e9

Commits on Jun 16, 2019

• Direct limit of modules, abelian groups, rings, and fields. (#754)

  Show description for 7b715eb
  

  kckennylau

  authored and

  mergify[bot]

  committed
  7b715eb

  Copy full SHA for 7b715eb

• feat(ring_theory/integral_closure): integral closure (#1087)

  Show description for 38d5c12
  

  kckennylau

  authored and

  mergify[bot]

  committed
  38d5c12

  Copy full SHA for 38d5c12

Commits on Jun 15, 2019

• feat(data/rat/denumerable): computable denumerability of Q (#1104)

  Show description for 3ad3522
  

  ChrisHughes24

  authored and

  mergify[bot]

  committed
  3ad3522

  Copy full SHA for 3ad3522

Commits on Jun 14, 2019

• feat(measure_theory/integration): dominated convergence theorem (#1123)

  Show description for 5040c81
  

  Zhouhang Zhou

  authored and

  mergify[bot]

  committed
  5040c81

  Copy full SHA for 5040c81

• provide some proof terms explicitly (#1132)

  

  urkud

  authored and

  mergify[bot]

  committed
  5a183f0

  Copy full SHA for 5a183f0

Commits on Jun 12, 2019

• chore(algebra/group/hom): drop unused section variables (#1130)

  

  urkud

  authored and

  mergify[bot]

  committed
  0c627fb

  Copy full SHA for 0c627fb

Commits on Jun 11, 2019

• feat(data/mv_polynomial): misc lemmas on rename, map, and eval2 (#1127)

  

  jcommelin

  authored and

  mergify[bot]

  committed
  3492206

  Copy full SHA for 3492206

• fix(category_theory): simplifying universes (#1122)

  

  kim-em

  authored and

  mergify[bot]

  committed
  953c612

  Copy full SHA for 953c612

• refactor(algebra/group): split into smaller files (#1121)

  Show description for 98ece77
  

  urkud

  authored and

  mergify[bot]

  committed
  98ece77

  Copy full SHA for 98ece77

• refactor(group_theory/abelianization): simplify abelianization (#1126)

  Show description for abfaf8d
  

  Michael-Howes

  authored and

  mergify[bot]

  committed
  abfaf8d

  Copy full SHA for abfaf8d

Commits on Jun 10, 2019

• feat(group_theory/presented_group): define presented groups (#1118)

  Show description for bd2f35f
  

  Michael-Howes

  authored and

  mergify[bot]

  committed
  bd2f35f

  Copy full SHA for bd2f35f

• feat (data/pnat): extensions to pnat (#1073)

  Show description for 004e0b3
  

  NeilStrickland

  authored and

  ChrisHughes24

  committed
  004e0b3

  Copy full SHA for 004e0b3

Commits on Jun 8, 2019

• feat(tactic/rewrite_all): tactic to perform the nth occurrence of a rewrite (#999)

  Show description for 3f9916e
  

  kim-em

  authored and

  mergify[bot]

  committed
  3f9916e

  Copy full SHA for 3f9916e

Commits on Jun 7, 2019

• refactor(analysis/normed_space/basic): change normed_space definition (#1112)

  

  sgouezel

  authored and

  mergify[bot]

  committed
  b55e44d

  Copy full SHA for b55e44d

• feat(data/quot): quot.map: act on non-id maps (#1120)

  Show description for 85ed958
  

  Yury G. Kudryashov

  authored and

  mergify[bot]

  committed
  85ed958

  Copy full SHA for 85ed958

Commits on Jun 6, 2019

• refactor(category_theory/equivalence): simplify equivalence.trans (#1114)

  

  rwbarton

  authored and

  mergify[bot]

  committed
  f36fdfb

  Copy full SHA for f36fdfb

Commits on Jun 5, 2019

• refactor(analysis/normed_space/operator_norm): topological modules (#1085)

  Show description for a7524b6
  

  sgouezel

  authored and

  mergify[bot]

  committed
  a7524b6

  Copy full SHA for a7524b6

Commits on Jun 4, 2019

• fix(data/logic/basic): Use a Sort for classical.some_spec2 (#1111)

  ChrisHughes24

  authored
  542d25d

  Copy full SHA for 542d25d

Commits on Jun 3, 2019

• feat(topology/basic): is_open_Inter and others (#1108)

  

  ChrisHughes24

  authored and

  mergify[bot]

  committed
  dd832f0

  Copy full SHA for dd832f0

• feat(data/set/basic): union_inter_distrib lemmas (#1107)

  Show description for 504c0ad
  

  ChrisHughes24

  authored and

  mergify[bot]

  committed
  504c0ad

  Copy full SHA for 504c0ad

• fix(data/nat/gcd): correct order of arguments in nat.coprime_mul_iff_right (#1105)

  Show description for 4263b2b
  

  NeilStrickland

  authored and

  mergify[bot]

  committed
  4263b2b

  Copy full SHA for 4263b2b

Commits on Jun 1, 2019

• feat(data/mv_polynomial): add coeff for mv_polynomial (#1101)

  

  jcommelin

  authored and

  mergify[bot]

  committed
  38b8054

  Copy full SHA for 38b8054

Commits on May 31, 2019

• feat(topology/algebra/open_subgroup): basics on open subgroups (#1067)

  Show description for 4f6307e
  

  jcommelin

  authored and

  mergify[bot]

  committed
  4f6307e

  Copy full SHA for 4f6307e

• fix(data/nat/enat): change [] to {} in some lemmas (#1054)

  Show description for 6237939
  

  ChrisHughes24

  authored and

  mergify[bot]

  committed
  6237939

  Copy full SHA for 6237939

• feat(category_theory/monoidal): the monoidal category of types (#1100)

  Show description for 8ebea31
  

  kim-em

  authored and

  mergify[bot]

  committed
  8ebea31

  Copy full SHA for 8ebea31