mem_mulAntidiagonal — Mathlib

English

The mulAntidiagonal set consists exactly of those pairs (x, y) such that x is in s, y is in t, and x·y = a. Equivalently, for any x in α×α, x ∈ mulAntidiagonal s t a if and only if x.1 ∈ s, x.2 ∈ t, and x.1·x.2 = a.

Русский

Мультипликативная антидиагональ состоит ровно из пар (x, y), где x ∈ s, y ∈ t и x·y = a. Эквивалентно: для пары x = (x1, x2) верно x1 ∈ s, x2 ∈ t и x1·x2 = a.

LaTeX

$$$x ∈ mulAntidiagonal\, s\, t\, a \;\leftrightarrow\; x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 \cdot x.2 = a$$$

Lean4

@[to_additive (attr := simp)]
theorem mem_mulAntidiagonal : x ∈ mulAntidiagonal s t a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 * x.2 = a :=
  Iff.rfl

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