val_inv_apply — Mathlib

English

If x ∈ ∏_i M_i is a unit, then the i-th component of its inverse equals the inverse of the i-th component: (x^{-1})_i = (x_i)^{-1}.

Русский

Если x ∈ ∏_i M_i является единицей, то i-ая компонента его обратного равна обратному i-ой компоненты: (x^{-1})_i = (x_i)^{-1}.

LaTeX

$$ (x^{-1})_i = (x_i)^{-1} $$

Lean4

@[to_additive]
theorem val_inv_apply (hx : IsUnit x) (i : ι) : (hx.unit⁻¹).1 i = (hx.apply i).unit⁻¹ := by
  rw [← Units.inv_eq_val_inv, ← MulEquiv.val_inv_piUnits_apply]; congr; ext; rfl

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