mulDissociated_singleton — Mathlib

English

For any a in a commutative group α, MulDissociated({a}) is equivalent to a ≠ 1.

Русский

Для любого a в коммутативной группе α, MulDissociated({a}) эквивалентно a ≠ 1.

LaTeX

$$$$ \mathrm{MulDissociated}({a}) \iff a \neq 1. $$$$

Lean4

@[to_additive (attr := simp)]
theorem mulDissociated_singleton : MulDissociated ({ a } : Set α) ↔ a ≠ 1 := by
  simp [MulDissociated, setOf_or, -subset_singleton_iff, Finset.coe_subset_singleton]

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