Skip to content

Commit 42f1cf9

Browse files
committed
chore(Algebra/Group/Subgroup/Basic): tag instIsMulTorsionFree with to_additive (leanprover-community#34536)
Free `to_additive` that is missing for some reason. Co-authored-by: tb65536 <thomas.l.browning@gmail.com>
1 parent f8f80fe commit 42f1cf9

1 file changed

Lines changed: 1 addition & 0 deletions

File tree

Mathlib/Algebra/Group/Subgroup/Basic.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -216,6 +216,7 @@ theorem pi_eq_bot_iff (H : ∀ i, Subgroup (f i)) : pi Set.univ H = ⊥ ↔ ∀
216216

217217
end Pi
218218

219+
@[to_additive]
219220
instance instIsMulTorsionFree [IsMulTorsionFree G] : IsMulTorsionFree H where
220221
pow_left_injective n hn a b := by
221222
have := pow_left_injective hn (M := G) (a₁ := a) (a₂ := b)

0 commit comments

Comments
 (0)