basisOfPid_bot — Mathlib

English

The basis of the bottom submodule is the trivial pair ⟨0, Basis.empty⟩.

Русский

База нулевого подмодуля есть тривиальная пара ⟨0, Basis.empty⟩.

LaTeX

$$$\\text{basisOfPid } b\\; \\bot = \\langle 0, \\text{Basis.empty }\\rangle$$$

Lean4

theorem basisOfPid_bot {ι : Type*} [Finite ι] (b : Basis ι R M) : Submodule.basisOfPid b ⊥ = ⟨0, Basis.empty _⟩ :=
  by
  obtain ⟨n, b'⟩ := Submodule.basisOfPid b ⊥
  let e : Fin n ≃ Fin 0 := b'.indexEquiv (Basis.empty _ : Basis (Fin 0) R (⊥ : Submodule R M))
  obtain rfl : n = 0 := by simpa using Fintype.card_eq.mpr ⟨e⟩
  exact Sigma.eq rfl (Basis.eq_of_apply_eq <| finZeroElim)

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