mulEquivOfMulEquiv_eq_map_apply — Mathlib

English

If the underlying map of the induced isomorphism equals the original map composed with a transfer along j, then the two constructions coincide on the nose.

Русский

Если тождественная часть отображения у индуктивного изоморфизма равна исходному отображению, композиция совпадает на точке.

LaTeX

$$$(f.mulEquivOfMulEquiv k H).toMonoidHom = f.map (\lambda y: y \in T) k$$$

Lean4

@[to_additive (attr := simp)]
theorem mulEquivOfMulEquiv_eq_map_apply {k : LocalizationMap T Q} {j : M ≃* P} (H : S.map j.toMonoidHom = T) (x) :
    f.mulEquivOfMulEquiv k H x = f.map (fun y : S ↦ show j.toMonoidHom y ∈ T from H ▸ Set.mem_image_of_mem j y.2) k x :=
  rfl

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