domDomCongrₗ_toAddEquiv — Mathlib

English

The AddEquiv underlying map of domDomCongr_ℓ agrees with the additive equivalence domDomCongrEquiv σ on the level of additive structure.

Русский

Пусть подложная подстановка AddEquiv для domDomCongr_ℓ совпадает с эквивалентностью domDomCongrEquiv σ на уровне аддитивной структуры.

LaTeX

$$$(\\uparrow(\\operatorname{domDomCongr}_{\\ell} S \\sigma)) = \\operatorname{domDomCongrEquiv}(\\sigma)$.$$

Lean4

@[simp]
theorem domDomCongrₗ_toAddEquiv (σ : ι ≃ ι') :
    (↑(domDomCongrₗ S σ : M [⋀^ι]→ₗ[R] N ≃ₗ[S] _) : M [⋀^ι]→ₗ[R] N ≃+ _) = domDomCongrEquiv σ :=
  rfl

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