congr — Mathlib

English

If M′ is linearly isomorphic to M″ as R-modules, then their quotients by rM′ and rM″ are isomorphic as R-modules.

Русский

Если M′ и M″ изоморфны как модули над R, то их квартиант-капторы rM′ и rM″ изоморфны как модули над R.

LaTeX

$$$$ \text{If } M' \cong_R M'', \; \QuotSMulTop(r,M') \cong_R \QuotSMulTop(r,M''). $$$$

Lean4

/-- If `M'` is isomorphic to `M''` as `R`-modules, then `M'⧸rM'` is isomorphic to `M''⧸rM''`. -/
protected def congr (e : M' ≃ₗ[R] M'') : QuotSMulTop r M' ≃ₗ[R] QuotSMulTop r M'' :=
  Submodule.Quotient.equiv (r • ⊤) (r • ⊤) e <| (Submodule.map_pointwise_smul r _ e.toLinearMap).trans (by simp)

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