isTorsionBySet_singleton_iff — Mathlib

English

For any a, IsTorsionBySet {a} is equivalent to IsTorsionBy a.

Русский

Для любого a из R торион по {a} эквивалентен ториону по a.

LaTeX

$$$IsTorsionBySet\,R\,M\,{\{a\}} \;\iff\; IsTorsionBy\,R\,M\,a$$$

Lean4

@[simp]
theorem isTorsionBySet_singleton_iff : IsTorsionBySet R M { a } ↔ IsTorsionBy R M a :=
  by
  refine ⟨fun h x => @h _ ⟨_, Set.mem_singleton _⟩, fun h x => ?_⟩
  rintro ⟨b, rfl : b = a⟩; exact @h _

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