iso_apply_mk — Mathlib

English

Applying the isomorphism to a representative mk m s yields the corresponding element in the target given by the unit-adjusted f(m).

Русский

Применение изоморфизма к представителю mk m s даёт соответствующий элемент в целевом модуле, полученный после применения f к m с поправкой на единицу.

LaTeX

$$$$ (\mathrm{iso}~S~f)(\mathrm{LocalizedModule.mk}(m,s)) = (\mathrm{map\_units} f s)^{-1}(f(m)). $$$$

Lean4

theorem iso_apply_mk (m : M) (s : S) :
    iso S f (LocalizedModule.mk m s) = (IsLocalizedModule.map_units f s).unit⁻¹.val (f m) :=
  rfl

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