mulDissociated_inv — Mathlib

English

Let S be a subset of a commutative group. The property of being multiplicatively dissociated is preserved under inversion: S is dissociated iff S inverted, i.e. S^{-1}, is dissociated.

Русский

Пусть S — подмножество коммутативной группы. Свойство мультипликативной диссоциации сохраняется при взятии обратной: S диссоциировано тогда и только тогда, когда S^{-1} диссоциировано.

LaTeX

$$$\text{Dissociated}(S^{-1}) \iff \text{Dissociated}(S)$$$

Lean4

@[to_additive (attr := simp)]
theorem mulDissociated_inv : MulDissociated s⁻¹ ↔ MulDissociated s :=
  (MulEquiv.inv α).mulDissociated_preimage

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