Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(linear_algebra): the direct sum of a submodule quotient is the quotient of the direct sum #17069

Closed
wants to merge 8 commits into from

It seems `linear_equiv.coe_trans` can't be `@[simp]` yet, or we'll ge…

a1b659b
Select commit
Loading
Failed to load commit list.
Closed

[Merged by Bors] - feat(linear_algebra): the direct sum of a submodule quotient is the quotient of the direct sum #17069

It seems `linear_equiv.coe_trans` can't be `@[simp]` yet, or we'll ge…
a1b659b
Select commit
Loading
Failed to load commit list.

Workflow runs completed with no jobs