symm_comp_ofMulEquivOfLocalizations_apply

English

For any k: N ≃* P, the equality k.symm (f.ofMulEquivOfLocalizations k x) = f x holds for all x, i.e., applying f followed by the inverse of k recovers f.

Русский

Для любого k: N ≃* P выполняется k.symm (f.ofMulEquivOfLocalizations k x) = f x для всех x.

LaTeX

$$$k^{-1}\\bigl(f.ofMulEquivOfLocalizations(k, x)\\bigr) = f(x).$$$

Lean4

@[to_additive]
theorem symm_comp_ofMulEquivOfLocalizations_apply {k : N ≃* P} (x) : k.symm (f.ofMulEquivOfLocalizations k x) = f x :=
  k.symm_apply_apply (f x)

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