mulEquivOfLocalizations_left_inv — Mathlib

English

For a localization f and a MulEquiv k, we have f.mulEquivOfLocalizations (f.ofMulEquivOfLocalizations k) = k.

Русский

Для локализации f и мультиэквивалентности k выполняется f.mulEquivOfLocalizations (f.ofMulEquivOfLocalizations k) = k.

LaTeX

$$$ f.mulEquivOfLocalizations (f.ofMulEquivOfLocalizations k) = k $$$

Lean4

@[to_additive]
theorem mulEquivOfLocalizations_left_inv (k : N ≃* P) : f.mulEquivOfLocalizations (f.ofMulEquivOfLocalizations k) = k :=
  DFunLike.ext _ _ fun x ↦ DFunLike.ext_iff.1 (f.lift_of_comp k.toMonoidHom) x

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