mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

refactor(linear_algebra/clifford_algebra): relax typeclasses to semiring

Open eric-wieser opened this issue 3 years ago • 1 comments

This generalization isn't motivated by any particular result or generalization in the literature; rather, it's motivated by allowing exterior_algebra R M to be redefined as clifford_algebra 0, as this prevents all the results having to be duplicated.

  • [x] depends on: #14303

Open in Gitpod

See also #14819

eric-wieser avatar May 24 '22 10:05 eric-wieser

This PR/issue depends on:

  • ~~leanprover-community/mathlib#14303~~ By Dependent Issues (🤖). Happy coding!

mathlib-dependent-issues-bot avatar Jun 17 '22 16:06 mathlib-dependent-issues-bot