units_val_iff — Mathlib

English

In Monoid M, SemiconjBy (a : M) x y for Units M is equivalent to SemiconjBy a x y; i.e., a semiconjugates x to y as a unit iff it does so in M.

Русский

В моноиде M полусопряжение SemiconjBy (a : M) x y для Units M эквивалентно SemiconjBy a x y; т.е. полусопряжение сохраняется в единицах и в M.

LaTeX

$$$$\forall a,x,y:\ SemiconjBy (a : M) x y \iff SemiconjBy a x y.$$$$

Lean4

@[to_additive (attr := simp)]
theorem units_val_iff {a x y : Mˣ} : SemiconjBy (a : M) x y ↔ SemiconjBy a x y :=
  ⟨units_of_val, units_val⟩

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