symm_comp_ofMulEquivOfLocalizations_apply'

English

If k is an isomorphism N ≃* P, then f.ofMulEquivOfLocalizations k.symm acts as the inverse on the image, i.e., k.symm (f.ofMulEquivOfLocalizations k x) = f x.

Русский

Если k — изоморфизм N ≃* P, то применяется обратное действие на образ: k.symm (f.ofMulEquivOfLocalizations k x) = f x.

LaTeX

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

Lean4

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

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