of_mulOpposite — Mathlib

English

UniqueProds is transferred through the opposite construction: UniqueProds Gᵐᵒᵖ implies/equals UniqueProds G.

Русский

Свойство UniqueProds переносится через противоположное: UniqueProds Gᵐᵒᵖ сохраняется для G.

LaTeX

$$$ \\forall G, \\mathrm{UniqueProds}(G^\\mathrm{op}) \\Rightarrow \\mathrm{UniqueProds}(G). $$$

Lean4

@[to_additive]
theorem of_mulOpposite (h : UniqueProds Gᵐᵒᵖ) : UniqueProds G where
  uniqueMul_of_nonempty hA
    hB :=
    let f : G ↪ Gᵐᵒᵖ := ⟨op, op_injective⟩
    let ⟨y, yB, x, xA, hxy⟩ := h.uniqueMul_of_nonempty (hB.map (f := f)) (hA.map (f := f))
    ⟨unop x, (mem_map' _).mp xA, unop y, (mem_map' _).mp yB, hxy.of_mulOpposite⟩

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