mathlib

2a7ceb0e - perf(linear_algebra): speed up `graded_algebra` instances (#14967)

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).