of_mulOpposite — Mathlib

English

From a unique-mul statement in opposite multiplication, deduce a unique-mul statement in the original multiplication.

Русский

Из уникальности разложения в противоположной группе выводим уникальность в исходной группе.

LaTeX

$$UniqueMul (B.map ⟨_, op_injective⟩) (A.map ⟨_, op_injective⟩) (op b0) (op a0) → UniqueMul A B a0 b0$$

Lean4

@[to_additive]
theorem of_mulOpposite (h : UniqueMul (B.map ⟨_, op_injective⟩) (A.map ⟨_, op_injective⟩) (op b0) (op a0)) :
    UniqueMul A B a0 b0 := fun a b aA bB ab ↦ by
  simpa [and_comm] using h (mem_map_of_mem _ bB) (mem_map_of_mem _ aA) (congr_arg op ab)

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