to_mulOpposite — Mathlib

English

Uniqueness is preserved when passing to the opposite multiplication via op map in the other direction.

Русский

Уникальность сохраняется при переходе к противоположной умножении через отображение op в другую сторону.

LaTeX

$$UniqueMul A B a0 b0 → UniqueMul (Finset.map { toFun := MulOpposite.op, inj' := ⋯ } B) (Finset.map { toFun := MulOpposite.op, inj' := ⋯ } A) (MulOpposite.op b0) (MulOpposite.op a0)$$

Lean4

@[to_additive]
theorem to_mulOpposite (h : UniqueMul A B a0 b0) :
    UniqueMul (B.map ⟨_, op_injective⟩) (A.map ⟨_, op_injective⟩) (op b0) (op a0) :=
  of_mulOpposite (by simp_rw [map_map]; exact (mulHom_map_iff _ fun _ _ ↦ by rfl).mpr h)

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