of_subsingleton — Mathlib

English

If G is subsingleton, then UniqueMul A B a0 b0 holds for any A,B and a0,b0.

Русский

Если G — пододиночное множество, то для любых A,B и a0,b0 выполняется UniqueMul.

LaTeX

$$$[\\text{Subsingleton } G] \\Rightarrow \\mathrm{UniqueMul}\\, A\\, B\\, a_0\\, b_0$$$

Lean4

@[to_additive (attr := nontriviality, simp)]
theorem of_subsingleton [Subsingleton G] : UniqueMul A B a0 b0 := by simp [UniqueMul, eq_iff_true_of_subsingleton]

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