ofEq — Mathlib

English

If two submodules are equal, there is a natural linear equivalence between their carrier subspaces.

Русский

Если два подмодуля равны, существует естественное линейное эквивалентное отображение между их носителями.

LaTeX

$$def ofEq (h : p = q) : p ≃_l[R] q$$

Lean4

/-- Linear equivalence between two equal submodules. -/
def ofEq (h : p = q) : p ≃ₗ[R] q :=
  { Equiv.setCongr (congr_arg _ h) with
    map_smul' := fun _ _ => rfl
    map_add' := fun _ _ => rfl }

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