English
If the codomain N of an injective monoid homomorphism is torsion-free, then the domain M is torsion-free as well.
Русский
Если кодомомандный образ инъективного моноидного гомоморфизма является безторсионным, то и доменная моноидная структура M безторсионна.
LaTeX
$$$$ IsMulTorsionFree M \text{ given } IsMulTorsionFree N \text{ and } f \text{ injective}. $$$$
Lean4
/-- If the codomain of an injective monoid homomorphism is torsion free,
then so is the domain. -/
@[to_additive /-- If the codomain of an injective additive monoid homomorphism is torsion free,
then so is the domain. -/
]
theorem isMulTorsionFree [Monoid M] [Monoid N] [IsMulTorsionFree N] (f : M →* N) (hf : Function.Injective f) :
IsMulTorsionFree M where
pow_left_injective n hn x y hxy := hf <| IsMulTorsionFree.pow_left_injective hn <| by simpa using congrArg f hxy
