ext — Mathlib

English

If two Grassmannian objects have equal underlying submodules, then they are equal as Grassmannian elements.

Русский

Если два элемента Grassmannian имеют одинаковые подмодули, то эти элементы равны как объекты Grassmannian.

LaTeX

$$$$ \forall N_1,N_2 \in G(k,M;R),\; (N_1 : \mathrm{Submodule}\; R M) = N_2 \Rightarrow N_1 = N_2. $$$$

Lean4

@[ext]
theorem ext {N₁ N₂ : G(k, M; R)} (h : (N₁ : Submodule R M) = N₂) : N₁ = N₂ := by cases N₁; cases N₂; congr 1

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