quotEquivOfEq — Mathlib

English

If p = p', then the quotient modules M/p and M/p' are linearly isomorphic via a natural linear equivalence provided by the quotient congruence.

Русский

Если p = p', то модули M/p и M/p' линейно изоморфны через естественное линейное эквивалентное отображение, задаваемое по эквивалентности факторов.

LaTeX

$$$(M/p) \cong_R (M/p')$ if $p = p'$$$

Lean4

/-- Quotienting by equal submodules gives linearly equivalent quotients. -/
def quotEquivOfEq (h : p = p') : (M ⧸ p) ≃ₗ[R] M ⧸ p' :=
  {
    @Quotient.congr _ _ (quotientRel p) (quotientRel p') (Equiv.refl _) fun a b =>
      by
      subst h
      rfl with
    map_add' := by
      rintro ⟨x⟩ ⟨y⟩
      rfl
    map_smul' := by
      rintro x ⟨y⟩
      rfl }

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