Code

An attempt at a quotient definition#11

Code

Draft

eric-wieser wants to merge 3 commits intopygae:utensil/new_designpygae/lean-ga:utensil/new_designfrom eric-wieser:tensor_quotienteric-wieser/lean-ga:tensor_quotientCopy head branch name to clipboard

+652-28

Commits

Commits on Jul 28, 2020

• Alternate proof formulation, maybe more readable?

  eric-wieser

  committed
  98a41b9

  Copy full SHA for 98a41b9

Commits on Jul 29, 2020

• tensor_algebra from upstream mathlib

  eric-wieser

  committed
  145364c

  Copy full SHA for 145364c

• Add an attempt at a clifford algebra via a quotient

  eric-wieser

  committed
  ca288b1

  Copy full SHA for ca288b1