iso_symm_apply' — Mathlib

English

If b · m = f(a) in the localized setting, then (iso S f)^{-1}(m) = LocalizedModule.mk(a,b).

Русский

Если b · m = f(a) в локализационном контексте, тогда (iso S f)^{-1}(m) = LocalizedModule.mk(a,b).

LaTeX

$$$$ (\mathrm{iso}~S~f)^{-1}(m) = \mathrm{LocalizedModule.mk}(a,b) \text{ if } b\cdot m = f(a). $$$$

Lean4

theorem iso_symm_apply' (m : M') (a : M) (b : S) (eq1 : b • m = f a) : (iso S f).symm m = LocalizedModule.mk a b :=
  (iso_symm_apply_aux S f m).trans <|
    LocalizedModule.mk_eq.mpr <| by
      rw [← IsLocalizedModule.eq_iff_exists S f, Submonoid.smul_def, Submonoid.smul_def, f.map_smul, f.map_smul, ←
        (surj _ _ _).choose_spec, ← Submonoid.smul_def, ← Submonoid.smul_def, ← mul_smul, mul_comm, mul_smul, eq1]

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