inv_op_smul_finset_distrib — Mathlib

English

Same as above with simplified form; membership equivalence under inverse smul distributes.

Русский

То же самое с упрощенной формой; принадлежность сохраняется под обратным переносом.

LaTeX

$$$(a \\cdot s)^{-1} = a^{-1} \\cdot s^{-1}$$$

Lean4

@[to_additive (attr := simp)]
theorem inv_op_smul_finset_distrib (a : α) (s : Finset α) : (op a • s)⁻¹ = a⁻¹ • s⁻¹ := by ext;
  simp [← inv_smul_mem_iff]

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