Skip to content

Commit

Permalink
chore: Algebra.Group fix smul align (#1435)
Browse files Browse the repository at this point in the history
  • Loading branch information
ChrisHughes24 committed Jan 9, 2023
1 parent 56bf534 commit 4b57ad6
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/Algebra/Group/Defs.lean
Expand Up @@ -77,7 +77,7 @@ class VSub (G : outParam (Type _)) (P : Type _) where
@[ext, to_additive]
class SMul (M : Type _) (α : Type _) where
smul : M → α → α
#align has_scalar SMul
#align has_smul SMul

instance instHVAdd [VAdd α β] : HVAdd α β β where
hVAdd := VAdd.vadd
Expand Down

0 comments on commit 4b57ad6

Please sign in to comment.