instSubsingletonDecomposition — Mathlib

English

The DirectSum.Decomposition data associated to a grading ℳ is unique; any two such decompositions are equal.

Русский

Данные декомпозиции DirectSum, соответствующие градации ℳ, уникальны: любые две такие декомпозиции равны.

LaTeX

$$DirectSum.Decomposition ℳ is a Subsingleton.$$

Lean4

/-- `DirectSum.Decomposition` instances, while carrying data, are always equal. -/
instance : Subsingleton (Decomposition ℳ) :=
  ⟨fun x y ↦ by
    obtain ⟨_, _, xr⟩ := x
    obtain ⟨_, yl, _⟩ := y
    congr
    exact Function.LeftInverse.eq_rightInverse xr yl⟩

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