ofMulEquivOfLocalizations_eq_iff_eq

English

For f and k as above, x maps to y under f.ofMulEquivOfLocalizations k if and only if under f, x maps to k.symm y.

Русский

Для f и k верна эквивалентность: f.ofMulEquivOfLocalizations k x = y тогда и только тогда, когда f x = k.symm y.

LaTeX

$$$ f.ofMulEquivOfLocalizations(k, x) = y \\quad\\text{iff}\\quad f(x) = k^{-1}(y).$$$

Lean4

@[to_additive]
theorem ofMulEquivOfLocalizations_eq_iff_eq {k : N ≃* P} {x y} : f.ofMulEquivOfLocalizations k x = y ↔ f x = k.symm y :=
  k.toEquiv.eq_symm_apply.symm

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