Skip to content

Commit

Permalink
fix: add default_instance attribute to instHSMul and instHVAdd (#1501)
Browse files Browse the repository at this point in the history
  • Loading branch information
fpvandoorn committed Jan 12, 2023
1 parent df20ea2 commit b6e6cc0
Showing 1 changed file with 8 additions and 8 deletions.
16 changes: 8 additions & 8 deletions Mathlib/Algebra/Group/Defs.lean
Expand Up @@ -79,21 +79,21 @@ class SMul (M : Type _) (α : Type _) where
smul : M → α → α
#align has_smul SMul

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

instance instHSMul [SMul α β] : HSMul α β β where
hSMul := SMul.smul

infixl:65 " +ᵥ " => HVAdd.hVAdd
infixl:65 " -ᵥ " => VSub.vsub
infixr:73 " • " => HSMul.hSMul

attribute [to_additive] Mul Div HMul instHMul HDiv instHDiv instHSMul HSMul
attribute [to_additive (reorder := 1)] Pow instHPow HPow
attribute [to_additive] Mul Div HMul instHMul HDiv instHDiv HSMul
attribute [to_additive (reorder := 1)] Pow HPow
attribute [to_additive (reorder := 1 5)] HPow.hPow
attribute [to_additive (reorder := 1 4)] Pow.pow

@[to_additive (attr := default_instance)]
instance instHSMul [SMul α β] : HSMul α β β where
hSMul := SMul.smul

attribute [to_additive (reorder := 1)] instHPow

universe u

variable {G : Type _}
Expand Down

0 comments on commit b6e6cc0

Please sign in to comment.