mathlib3
refactor(data/real/basic): golf the ring instance
#8146
Open
Overview
Commits
38
Changes
View On GitHub
Commits
  • chore(data/real/basic): add missing lemmas about `cauchy` and `of_cauchy`
    eric-wieser committed 4 years ago
  • fixup
    eric-wieser committed 4 years ago
  • Merge branch 'master' into eric-wieser/real.comm_ring
    eric-wieser committed 4 years ago
  • Merge branch 'master' into eric-wieser/real.comm_ring
    eric-wieser committed 3 years ago
  • Merge branch 'master' into eric-wieser/real.comm_ring
    eric-wieser committed 3 years ago
  • fix
    eric-wieser committed 3 years ago
  • fix
    eric-wieser committed 3 years ago
  • Merge remote-tracking branch 'origin/master' into eric-wieser/real.comm_ring
    eric-wieser committed 3 years ago
  • wip
    eric-wieser committed 3 years ago
  • Merge remote-tracking branch 'origin/master' into eric-wieser/real.comm_ring
    eric-wieser committed 3 years ago
  • fix
    eric-wieser committed 3 years ago
  • fix
    eric-wieser committed 3 years ago
  • pow_zero is no longer true by rfl
    eric-wieser committed 3 years ago
  • Merge remote-tracking branch 'origin/master' into eric-wieser/real.comm_ring
    eric-wieser committed 3 years ago
  • reduce diff
    eric-wieser committed 3 years ago
  • fix
    eric-wieser committed 3 years ago
  • workaround abel bug
    eric-wieser committed 3 years ago
  • fix: zpow is not defeq to npow any more
    eric-wieser committed 3 years ago
  • revert old change
    eric-wieser committed 3 years ago
  • adjust comment, fix diamond
    eric-wieser committed 3 years ago
  • fix a broken convert
    eric-wieser committed 3 years ago
  • fix
    eric-wieser committed 3 years ago
  • fix
    eric-wieser committed 3 years ago
  • fix
    eric-wieser committed 3 years ago
  • fix
    eric-wieser committed 3 years ago
  • fix timeout
    eric-wieser committed 3 years ago
  • fix
    eric-wieser committed 3 years ago
  • fix
    eric-wieser committed 3 years ago
  • chore(*): remove some defeq abuse of `^`
    eric-wieser committed 3 years ago
  • Merge remote-tracking branch 'origin/master' into eric-wieser/real.comm_ring
    eric-wieser committed 3 years ago
  • remove workarounds now that the fix is in
    eric-wieser committed 3 years ago
  • Merge remote-tracking branch 'origin/eric-wieser/real.comm_ring-basics' into eric-wieser/real.comm_ring
    eric-wieser committed 3 years ago
  • Merge remote-tracking branch 'origin/master' into eric-wieser/real.comm_ring
    eric-wieser committed 3 years ago
  • fix(tactic/ring): perform definitional rather than syntactic matches on `^`
    eric-wieser committed 3 years ago
  • Merge remote-tracking branch 'origin/eric-wieser/fix-ring' into eric-wieser/real.comm_ring
    eric-wieser committed 3 years ago
  • squeeze a simp
    eric-wieser committed 3 years ago
  • Merge remote-tracking branch 'origin/master' into eric-wieser/real.comm_ring
    eric-wieser committed 3 years ago
  • Merge remote-tracking branch 'origin/master' into eric-wieser/real.comm_ring
    eric-wieser committed 3 years ago
FAQ Terms Privacy Refunds Impressum
Loading