bot — Mathlib

English

Equivalence modulo the bottom subspace is trivial: two elements are equivalent if and only if they are equal.

Русский

Эквивалентность по модулю нижнего подпространства тривиальна: два элемента равны тогда и только тогда, когда равны.

LaTeX

$$$ x \\equiv y [SMOD (\\perp : Submodule R M)] \\iff x = y$$$

Lean4

@[simp]
theorem bot : x ≡ y [SMOD (⊥ : Submodule R M)] ↔ x = y := by
  rw [SModEq.def, Submodule.Quotient.eq, mem_bot, sub_eq_zero]

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