subsingleton — Mathlib

English

Addition on LocalizedModule is defined by liftOn₂ using mk construction and compatibility via mk_eq.

Русский

Сложение в LocalizedModule задаётся через liftOn₂ с использованием mk и совместимости через mk_eq.

LaTeX

$$$a + b = \\text{liftOn}_2(a,b)(\\text{mk})$ with mk_eq compatibility.$$

Lean4

/-- If `S` contains `0` then the localization at `S` is trivial. -/
theorem subsingleton (h : 0 ∈ S) : Subsingleton (LocalizedModule S M) :=
  by
  refine ⟨fun a b ↦ ?_⟩
  induction a, b using LocalizedModule.induction_on₂
  exact mk_eq.mpr ⟨⟨0, h⟩, by simp only [Submonoid.mk_smul, zero_smul]⟩

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