subsingleton — Mathlib

English

Under UniqueMul A B a0 b0, the set of representations (a,b) with a∈A, b∈B, a*b=a0*b0 is subsingleton.

Русский

При UniqueMul A B a0 b0 множество представлений (a,b) имеет не более одного элемента.

LaTeX

$$Same as 12241$$

Lean4

@[to_additive]
theorem subsingleton (h : UniqueMul A B a0 b0) :
    Subsingleton { ab : G × G // ab.1 ∈ A ∧ ab.2 ∈ B ∧ ab.1 * ab.2 = a0 * b0 } :=
  ⟨fun ⟨⟨_a, _b⟩, ha, hb, ab⟩ ⟨⟨_a', _b'⟩, ha', hb', ab'⟩ ↦
    Subtype.ext <|
      Prod.ext ((h ha hb ab).1.trans (h ha' hb' ab').1.symm) <| (h ha hb ab).2.trans (h ha' hb' ab').2.symm⟩

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