submodule_unique

Mathlib.LinearAlgebra.Projection

URI: https://scilib.ai/kg/mathlib#LinearMap.IsProj.submodule_unique

← MathLib Explorer

English

If two projections m1 f and m2 f yield IsProj, then m1 = m2.

Русский

Если две проекции m1 f и m2 f дают IsProj, то m1 = m2.

LaTeX

$$If hf1: IsProj m1 f and hf2: IsProj m2 f then m1 = m2.$$

Lean4

theorem submodule_unique {f : M →ₗ[S] M} {m₁ m₂ : Submodule S M} (hf₁ : IsProj m₁ f) (hf₂ : IsProj m₂ f) : m₁ = m₂ := by
  ext; simp [hf₁.mem_iff_map_id, hf₂.mem_iff_map_id]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru