iff_mulOpposite — Mathlib

English

UniqueMul A B a0 b0 is equivalent to UniqueMul (B.map op) (A.map op) (op b0) (op a0).

Русский

UniqueMul A B a0 b0 эквивалентно UniqueMul (B.map op) (A.map op) (op b0) (op a0).

LaTeX

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

Lean4

@[to_additive]
theorem iff_mulOpposite :
    UniqueMul (B.map ⟨_, op_injective⟩) (A.map ⟨_, op_injective⟩) (op b0) (op a0) ↔ UniqueMul A B a0 b0 :=
  ⟨of_mulOpposite, to_mulOpposite⟩

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