instIsMulTorsionFree — Mathlib

English

If G is torsion-free, then any subgroup H ≤ G is torsion-free.

Русский

Если G безторможенная, тогда любая подгруппа H ≤ G также безторможенная.

LaTeX

$$$ \text{If } \text{IsMulTorsionFree}(G) \text{ then } \text{IsMulTorsionFree}(H) $$$

Lean4

instance instIsMulTorsionFree [IsMulTorsionFree G] : IsMulTorsionFree H where
  pow_left_injective n hn a
    b := by
    have := pow_left_injective hn (M := G) (a₁ := a) (a₂ := b)
    dsimp at *
    norm_cast at this

Похожие утверждения