units_inv_right_iff — Mathlib

English

For unit a, SemiconjBy a ↑x⁻¹ ↑y⁻¹ is equivalent to SemiconjBy a x y.

Русский

Для единицы a полусопряжение SemiconjBy a ↑x⁻¹ ↑y⁻¹ эквивалентно SemiconjBy a x y.

LaTeX

$$$$\forall a\in M^{\times},\ x,y\in M:\ SemiconjBy a \uparrow x^{-1} \uparrow y^{-1} \iff SemiconjBy a x y.$$$$

Lean4

@[to_additive (attr := simp)]
theorem units_inv_right_iff {a : M} {x y : Mˣ} : SemiconjBy a ↑x⁻¹ ↑y⁻¹ ↔ SemiconjBy a x y :=
  ⟨units_inv_right, units_inv_right⟩

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