Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
perf(linear_algebra): speed up
graded_algebra
instances (#14967)
Reduce `elaboration of graded_algebra` in: + `exterior_algebra.graded_algebra` from ~20s to 3s- + `tensor_algebra.graded_algebra` from 7s+ to 2s- + `clifford_algebra.graded_algebra` from 14s+ to 4s- (These numbers were before `lift_ι` and `lift_ι_eq` were extracted from `exterior_algebra.graded_algebra` and `lift_ι_eq` was extracted from `clifford_algebra.graded_algebra` in #12182.) Fix [timeout reported on Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/deterministic.20timeout/near/286996731) Also shorten the statements of the first two without reducing clarity (I think).
- Loading branch information
1 parent
a5a6865
commit 2a7ceb0
Showing
3 changed files
with
22 additions
and
20 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters