Commit 2024-02-14 01:35 1e659b6c
View on Github →feat: HahnModule action by HahnSeries (#10164)
Given a SMul R V instance, we introduce HahnModule Γ R V as an alias for HahnSeries Γ V, and produce a SMul (HahnSeries Γ R) (HahnModule Γ R V) instance. We use the SMul instance to shorten the Mul instance. We will work our way up to Module (HahnSeries Γ R) (HahnModule Γ R V) in a later PR.