liftQSpanSingleton — Mathlib

English

The quotient by the top submodule ⊤ is unique (a singleton).

Русский

Фактор-модуль по верхнему подмодулю ⊤ является уникальным (одиночным).

LaTeX

$$$$ M / \\top \\text{ is unique (singleton).} $$$$

Lean4

/-- Special case of `submodule.liftQ` when `p` is the span of `x`. In this case, the condition on
`f` simply becomes vanishing at `x`. -/
def liftQSpanSingleton (x : M) (f : M →ₛₗ[τ₁₂] M₂) (h : f x = 0) : (M ⧸ R ∙ x) →ₛₗ[τ₁₂] M₂ :=
  (R ∙ x).liftQ f <| by rw [span_singleton_le_iff_mem, LinearMap.mem_ker, h]

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