spanRank_eq_zero_iff_eq_bot — Mathlib

English

A submodule I has spanRank zero if and only if I is the bottom submodule.

Русский

Подмодуль I имеет spanRank = 0 тогда и только тогда, когда I = ⊥.

LaTeX

$$$I.spanRank = 0 \iff I = \bot$$$

Lean4

@[simp]
theorem spanRank_eq_zero_iff_eq_bot {I : Submodule R M} : I.spanRank = 0 ↔ I = ⊥ :=
  by
  constructor
  · intro h
    obtain ⟨s, ⟨hs₁, hs₂⟩⟩ := (FG.spanRank_le_iff_exists_span_set_card_le I (a := 0)).mp (by rw [h])
    simp only [nonpos_iff_eq_zero, mk_eq_zero_iff, Set.isEmpty_coe_sort] at hs₁
    simp_all
  · rintro rfl; rw [spanRank]
    exact Cardinal.iInf_eq_zero_iff.mpr (Or.inr ⟨⟨∅, by simp⟩, by simp⟩)

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