Commits

Branch selector

 master

User selector

All users

All time

Commit history

Commits on Jan 12, 2019

• fix(field_theory/subfield): is_subfield should be a Prop (#588)

  

  ChrisHughes24

  authored and

  digama0

  committed
  dc6c38a

  Copy full SHA for dc6c38a

Commits on Jan 11, 2019

• feat(ring_theory/euclidean_domain): add more specific Euclidean domain stuff (#527)

  

  ChrisHughes24

  authored and

  johoelzl

  committed
  e61a464

  Copy full SHA for e61a464

• feat(category_theory): over and under categories (#549)

  

  jcommelin

  authored and

  johoelzl

  committed
  5c323cd

  Copy full SHA for 5c323cd

• feat(meta/rb_map): add some monadic filtering

  

  cipher1024

  authored and

  johoelzl

  committed
  c19b4be

  Copy full SHA for c19b4be

• Update PULL_REQUEST_TEMPLATE.md

  

  robertylewis

  authored and

  johoelzl

  committed
  7a9b2e4

  Copy full SHA for 7a9b2e4

• doc(README): elect new maintainers

  johoelzl

  committed
  6516c34

  Copy full SHA for 6516c34

• chore(ring_theory/subring): remove unused import

  

  ChrisHughes24

  authored and

  johoelzl

  committed
  4f3f86d

  Copy full SHA for 4f3f86d

• feat(data/polynomial): various lemmas about degree and monic and coeff

  

  kckennylau

  authored and

  johoelzl

  committed
  4578796

  Copy full SHA for 4578796

Commits on Jan 10, 2019

• fix(principal_ideal_domain): correct spelling mistake (#582)

  

  ChrisHughes24

  authored and

  digama0

  committed
  b1684fe

  Copy full SHA for b1684fe

• refactor(principal_ideal_domain): simplify proof of PID -> UFD

  

  Chris Hughes

  authored and

  johoelzl

  committed
  6e97721

  Copy full SHA for 6e97721

• refactor(unique_factorization_domain): simplify definition of UFD

  

  Chris Hughes

  authored and

  johoelzl

  committed
  f5bf277

  Copy full SHA for f5bf277

• functions and cardinality (#556)

  

  sgouezel

  authored and

  johoelzl

  committed
  8b66ebd

  Copy full SHA for 8b66ebd

Commits on Jan 9, 2019

• chore(tactic/monotonicity/interactive) use derive for has_reflect (#578)

  

  kckennylau

  authored and

  johoelzl

  committed
  f488635

  Copy full SHA for f488635

• feat(field_theory/finite): field_of_integral_domain (#579)

  

  ChrisHughes24

  authored and

  johoelzl

  committed
  af735a5

  Copy full SHA for af735a5

• feat(data/polynomial): lemmas about map (#530)

  

  ChrisHughes24

  authored and

  johoelzl

  committed
  d0532c1

  Copy full SHA for d0532c1

Commits on Jan 5, 2019

• feat(group_theory/subgroup): simple groups (#572)

  

  ChrisHughes24

  authored and

  digama0

  committed
  2e63635

  Copy full SHA for 2e63635

• feat(data/fintype): decidable_left_inverse_fintype (#575)

  

  ChrisHughes24

  authored and

  digama0

  committed
  d19c9bc

  Copy full SHA for d19c9bc

• feat(group_theory/sign): sign_surjective (#576)

  

  ChrisHughes24

  authored and

  digama0

  committed
  395aadd

  Copy full SHA for 395aadd

• feat(ring_theory/multiplicity): multiplicity of elements of a ring (#523)

  

  ChrisHughes24

  authored and

  digama0

  committed
  b9c5eb0

  Copy full SHA for b9c5eb0

• feat(group_theory/quotient_group): quotient_ker_equiv_range (#574)

  

  ChrisHughes24

  authored and

  digama0

  committed
  bc96eca

  Copy full SHA for bc96eca

• feat(data/polynomial): polynomials over a field are a normalization domain (#560)

  

  ChrisHughes24

  authored and

  digama0

  committed
  3ff5e93

  Copy full SHA for 3ff5e93

• feat(data/polynomial): C_neg and C_sub (#561)

  

  ChrisHughes24

  authored and

  digama0

  committed
  87bf618

  Copy full SHA for 87bf618

• feat(data/multiset): prod_hom and exists_mem_of_rel_of_mem (#562)

  

  ChrisHughes24

  authored and

  digama0

  committed
  78d0ebf

  Copy full SHA for 78d0ebf

• feat(ring_theory/noetherian): irreducible_induction_on (#563)

  

  ChrisHughes24

  authored and

  digama0

  committed
  4e509a8

  Copy full SHA for 4e509a8

• doc(category_theory): update `category_theory` documentation (#564) [ci-skip]

  

  cipher1024

  authored and

  digama0

  committed
  ea0ff05

  Copy full SHA for ea0ff05

• feat(data/nat/enat): has_well_founded for enat (#565)

  

  ChrisHughes24

  authored and

  digama0

  committed
  33df7ec

  Copy full SHA for 33df7ec

• feat(logic/basic): inhabited_of_nonempty with instance parameter (#566)

  

  sgouezel

  authored and

  digama0

  committed
  4bacdf2

  Copy full SHA for 4bacdf2

• feat(data/multiset): forall_of_pairwise (#569)

  

  ChrisHughes24

  authored and

  digama0

  committed
  125feb6

  Copy full SHA for 125feb6

• feat(algebra/group): is_conj_one_right (#570)

  

  ChrisHughes24

  authored and

  digama0

  committed
  da6ec21

  Copy full SHA for da6ec21

• feat(data/finset): finset.card_eq_one (#571)

  

  ChrisHughes24

  authored and

  digama0

  committed
  a32fa18

  Copy full SHA for a32fa18

• fix(analysis/measure_theory): fix build

  digama0

  committed
  40fa9ad

  Copy full SHA for 40fa9ad

• fix(data/real/cau_seq_filter): fix build

  digama0

  committed
  93a330e

  Copy full SHA for 93a330e

• feat(analysis/topology): Bounded continuous functions (#464)

  

  sgouezel

  authored and

  digama0

  committed
  19e7b1f

  Copy full SHA for 19e7b1f

Commits on Jan 2, 2019

• feat(analysis/topology): complete sets, minor modifications (#557)

  

  sgouezel

  authored and

  digama0

  committed
  dcd0466

  Copy full SHA for dcd0466

• feat(data/real/ennreal): minor additions to ennreal (#558)

  

  sgouezel

  authored and

  digama0

  committed
  f59f5d5

  Copy full SHA for f59f5d5