inv_smul_finset_distrib₀ — Mathlib

English

The inverse of a smul Finset distributes: (a · s)^{-1} = a^{-1} · s^{-1}.

Русский

Обратное к умножению множества распределяется: (a · s)^{-1} = a^{-1} · s^{-1}.

LaTeX

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

Lean4

@[simp]
theorem inv_smul_finset_distrib₀ (a : α) (s : Finset α) : (a • s)⁻¹ = s⁻¹ <• a⁻¹ :=
  by
  obtain rfl | ha := eq_or_ne a 0
  ·
    obtain rfl | hs := s.eq_empty_or_nonempty <;>
      simp [*]
        -- was `simp` and very slow (https://github.com/leanprover-community/mathlib4/issues/19751)

  · ext;
    simp only [mem_inv', ne_eq, not_false_eq_true, ← inv_smul_mem_iff₀, smul_eq_mul, MulOpposite.op_inv, inv_eq_zero,
      MulOpposite.op_eq_zero_iff, inv_inv, MulOpposite.smul_eq_mul_unop, MulOpposite.unop_op, mul_inv_rev, ha]

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