spanFinrank_eq_zero_iff_eq_bot — Mathlib

English

If p is finitely generated, then spanFinrank(p) = 0 if and only if p = bottom (⊥).

Русский

Если p конечно порождается, то spanFinrank(p) = 0 тогда и только тогда, когда p = ⊥.

LaTeX

$$$p.\mathrm{spanFinrank} = 0 \iff p = \bot\quad (p\text{ is FG}).$$$

Lean4

theorem spanFinrank_eq_zero_iff_eq_bot {p : Submodule R M} (h : p.FG) : p.spanFinrank = 0 ↔ p = ⊥ :=
  by
  refine ⟨fun heq ↦ ?_, fun h ↦ h ▸ by simp⟩
  rw [← Submodule.FG.generators_ncard h, Set.ncard_eq_zero h.finite_generators] at heq
  rw [← p.span_generators, heq, span_empty]

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