semiconjBy_iff_eq — Mathlib

English

Over a CancelCommMonoid, SemiconjBy a x y is equivalent to x = y.

Русский

В CancelCommMonoid semiconjugacy между a, x, y эквивалентна равенству x = y.

LaTeX

$$$$\text{In a CancelCommMonoid } M,\ SemiconjBy\ a\ x\ y \iff x = y.$$$$

Lean4

@[to_additive (attr := simp)]
theorem semiconjBy_iff_eq [CancelCommMonoid M] {a x y : M} : SemiconjBy a x y ↔ x = y :=
  ⟨fun h => mul_left_cancel (h.trans (mul_comm _ _)), fun h => by rw [h, SemiconjBy, mul_comm]⟩

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