prod_inv — Mathlib

English

If h_i( f_i ) = 1 for all i, then f.prod h = 1.

Русский

Если для всех i выполнено h_i( f_i ) = 1, то f.prod h = 1.

LaTeX

$$$\\forall i, h i (f i) = 1 \\implies f.prod h = 1$$$

Lean4

@[to_additive (attr := simp)]
theorem prod_inv [∀ i, AddCommMonoid (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] [DivisionCommMonoid γ] {f : Π₀ i, β i}
    {h : ∀ i, β i → γ} : (f.prod fun i b => (h i b)⁻¹) = (f.prod h)⁻¹ :=
  (map_prod (invMonoidHom : γ →* γ) _ f.support).symm

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