Commits

Breadcrumbs

History for

onmaster

User selector

All users

All time

Commit history

Commits on Nov 5, 2018

• refactor(cau_seq): unify real.lim, complex.lim and cau_seq.lim (#433)

  

  ChrisHughes24

  authored and

  johoelzl

  committed
  53d4883

  Copy full SHA for 53d4883

• feat(linear_algebra,ring_theory): refactoring modules (#456)

  Show description for a12d5a1
  digama0

  committed
  a12d5a1

  Copy full SHA for a12d5a1

• feat(data/real/irrational): add basic irrational facts (#453)

  Show description for 8898f0e
  

  abhimanyupallavisudhir

  authored and

  digama0

  committed
  8898f0e

  Copy full SHA for 8898f0e

• refactor(data/real/basic): make real irreducible (#454)

  

  ChrisHughes24

  authored and

  digama0

  committed
  94b09d6

  Copy full SHA for 94b09d6

Commits on Oct 18, 2018

• cleanup(data/nat/choose,binomial): move binomial into choose

  johoelzl

  committed
  7b876a2

  Copy full SHA for 7b876a2

Commits on Oct 2, 2018

• feat(data/padics): use prime typeclass

  

  robertylewis

  authored and

  johoelzl

  committed
  1562cc2

  Copy full SHA for 1562cc2

• feat(data/real/cau_seq): relate cauchy sequence completeness and filter completeness

  

  robertylewis

  authored and

  johoelzl

  committed
  e6a1bc3

  Copy full SHA for e6a1bc3

• feat(data/padics): prove Hensel's lemma

  

  robertylewis

  authored and

  johoelzl

  committed
  e0b0c53

  Copy full SHA for e0b0c53

• feat(data/padics): use has_norm typeclasses for padics

  

  robertylewis

  authored and

  johoelzl

  committed
  f040aef

  Copy full SHA for f040aef

Commits on Sep 13, 2018

• fix(data/padics/padic_rationals): fix proof

  digama0

  committed
  a770ee5

  Copy full SHA for a770ee5

Commits on Sep 3, 2018

• fix(*): fix simpa uses

  digama0

  committed
  4de119e

  Copy full SHA for 4de119e

• refactor(tactic/interactive): improve error reporting for simpa

  Show description for 956398c
  digama0

  committed
  956398c

  Copy full SHA for 956398c

Commits on Aug 31, 2018

• refactor(data/int/gcd): move int gcd proofs to the GCD theory

  johoelzl

  committed
  5df7cac

  Copy full SHA for 5df7cac

Commits on Aug 30, 2018

• refactor(data/nat,int): separate int from nat, i.e. do not import any int theory in nat

  johoelzl

  committed
  83edcc0

  Copy full SHA for 83edcc0

Commits on Aug 16, 2018

• fix(padics/padic_norm): remove spurious import

  digama0

  committed
  12d103c

  Copy full SHA for 12d103c

• feat(data/padics): p-adic numbers (#262)

  

  robertylewis

  authored and

  digama0

  committed
  93817f1

  Copy full SHA for 93817f1

Loading