semiconjBy_iff — Mathlib

English

For M,N with multiplication, SemiconjBy on the product M × N is equivalent to semiconjugacy on each coordinate.

Русский

Для произведения M × N условие semiconjugacy эквивалентно условию semiconjugacy по каждой координате.

LaTeX

$$$\text{SemiconjBy}(x,y,z) \iff (\text{SemiconjBy}(x_1,y_1,z_1) \wedge \text{SemiconjBy}(x_2,y_2,z_2))$$$

Lean4

@[to_additive]
theorem semiconjBy_iff {x y z : M × N} : SemiconjBy x y z ↔ SemiconjBy x.1 y.1 z.1 ∧ SemiconjBy x.2 y.2 z.2 :=
  Prod.ext_iff

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