mathlib3
refactor(linear_algebra/clifford_algebra): relax typeclasses to semiring
#14350
Open
Overview
Commits
45
Changes
View On GitHub
Commits
  • wip
    eric-wieser committed 3 years ago
  • Merge remote-tracking branch 'origin/master' into eric-wieser/quadratic_form-semiring
    eric-wieser committed 3 years ago
  • wip
    eric-wieser committed 3 years ago
  • generalize to semiring
    eric-wieser committed 3 years ago
  • fix
    eric-wieser committed 3 years ago
  • fix
    eric-wieser committed 3 years ago
  • remove dead code
    eric-wieser committed 3 years ago
  • another one
    eric-wieser committed 3 years ago
  • even more
    eric-wieser committed 3 years ago
  • last one (untested)
    eric-wieser committed 3 years ago
  • now build it again
    eric-wieser committed 3 years ago
  • more
    eric-wieser committed 3 years ago
  • Update dual.lean
    eric-wieser committed 3 years ago
  • Merge remote-tracking branch 'origin/eric-wieser/bilin_form-tweak' into eric-wieser/quadratic_form-semiring
    eric-wieser committed 3 years ago
  • fix build
    eric-wieser committed 3 years ago
  • feat(linear_algebra/quadratic_form/isometry): extract from `linear_algebra/quadratic_form/basic`
    eric-wieser committed 3 years ago
  • fix import
    eric-wieser committed 3 years ago
  • fix
    eric-wieser committed 3 years ago
  • Merge remote-tracking branch 'origin/master' into eric-wieser/bilin_form-tweak
    eric-wieser committed 3 years ago
  • Merge branch 'eric-wieser/bilin_form-tweak' into eric-wieser/quadratic_form-semiring
    eric-wieser committed 3 years ago
  • docstrings
    eric-wieser committed 3 years ago
  • Merge remote-tracking branch 'origin/eric-wieser/split-isometry' into eric-wieser/quadratic_form-semiring
    eric-wieser committed 3 years ago
  • chore(linear_algebra/quadratic_form/basic): Reorder lemmas
    eric-wieser committed 3 years ago
  • Merge branch 'eric-wieser/quadratic_form-move-fun_like' into eric-wieser/quadratic_form-semiring
    eric-wieser committed 3 years ago
  • Merge remote-tracking branch 'origin/master'
    eric-wieser committed 3 years ago
  • Merge branch into eric-wieser/quadratic_form-semiring
    eric-wieser committed 3 years ago
  • reorder
    eric-wieser committed 3 years ago
  • fix the build
    eric-wieser committed 3 years ago
  • Merge branch 'eric-wieser/quadratic_form-semiring' of https://github.com/leanprover-community/mathlib into eric-wieser/quadratic_form-semiring
    eric-wieser committed 3 years ago
  • fix
    eric-wieser committed 3 years ago
  • refactor(linear_algebra/clifford_algebra): relax typeclasses to semiring
    eric-wieser committed 3 years ago
  • Merge branch 'master' into eric-wieser/quadratic_form-semiring
    eric-wieser committed 3 years ago
  • sorry-free
    eric-wieser committed 3 years ago
  • Merge remote-tracking branch 'origin/staging' into eric-wieser/quadratic_form-semiring
    eric-wieser committed 3 years ago
  • add polar_bilin
    eric-wieser committed 3 years ago
  • Merge remote-tracking branch 'origin/staging' into eric-wieser/quadratic_form-semiring
    eric-wieser committed 3 years ago
  • golf
    eric-wieser committed 3 years ago
  • whitespace
    eric-wieser committed 3 years ago
  • Merge remote-tracking branch 'origin/master' into HEAD
    eric-wieser committed 3 years ago
  • Merge commit 'HEAD@{1}' into eric-wieser/clifford_algebra-semiring-redo
    eric-wieser committed 3 years ago
  • Update basic.lean
    eric-wieser committed 3 years ago
  • fix
    eric-wieser committed 3 years ago
  • remove irreducible
    eric-wieser committed 3 years ago
  • Remove redundant line
    eric-wieser committed 3 years ago
  • Merge remote-tracking branch 'origin/master' into eric-wieser/clifford_algebra-semiring-redo
    eric-wieser committed 3 years ago
FAQ Terms Privacy Refunds Impressum
Loading