op_eq_one_iff — Mathlib

English

In any type with a multiplicative identity, the opposite element op a equals 1 if and only if a equals 1.

Русский

В любой группе с умножением, у элемента a версия в противоположной структуре удовлетворяет: op a = 1 тогда и только тогда a = 1.

LaTeX

$$$ (\\mathrm{op}\\ a = 1) \\iff a = 1 $$$

Lean4

@[to_additive (attr := simp)]
theorem op_eq_one_iff [One α] (a : α) : op a = 1 ↔ a = 1 :=
  op_injective.eq_iff

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