swap_mem_mulAntidiagonal — Mathlib

English

If the ambient operation is commutative, swapping the two coordinates exchanges the left/right roles of s and t in the antidiagonal: x.swap ∈ mulAntidiagonal s t a iff x ∈ mulAntidiagonal t s a.

Русский

При коммутативности обмен координат меняет местами роли s и t в антидиагонали: x.swap ∈ mulAntidiagonal s t a ⇔ x ∈ mulAntidiagonal t s a.

LaTeX

$$$x.swap \in mulAntidiagonal\, s\, t\, a \;\iff\; x \in mulAntidiagonal\, t\, s\, a$ (при CommMagma).$$

Lean4

@[to_additive]
theorem swap_mem_mulAntidiagonal [CommMagma α] {s t : Set α} {a : α} {x : α × α} :
    x.swap ∈ Set.mulAntidiagonal s t a ↔ x ∈ Set.mulAntidiagonal t s a := by simp [mul_comm, and_left_comm]

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