Skip to content

chore(RingTheory/TensorProduct): golf the mul definition#6195

Open
eric-wieser wants to merge 2 commits into
masterfrom
tidy-RingTheory.tensor
Open

chore(RingTheory/TensorProduct): golf the mul definition#6195
eric-wieser wants to merge 2 commits into
masterfrom
tidy-RingTheory.tensor

Merge branch 'master' into tidy-RingTheory.tensor

a711a3a
Select commit
Loading
Failed to load commit list.

Workflow runs completed with no jobs