mem_smulAntidiagonal — Mathlib

English

An element x belongs to SMulAntidiagonal hs ht a exactly when x1 ∈ s, x2 ∈ t and x1 • x2 = a.

Русский

Элемент x принадлежит SMulAntidiagonal hs ht a тогда и только тогда, когда x1 ∈ s, x2 ∈ t и x1 • x2 = a.

LaTeX

$$$ x ∈ SMulAntidiagonal hs ht a \iff x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 • x.2 = a $$$

Lean4

@[to_additive (attr := simp)]
theorem mem_smulAntidiagonal : x ∈ SMulAntidiagonal hs ht a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 • x.2 = a :=
  by
  simp only [SMulAntidiagonal, Set.Finite.mem_toFinset]
  exact Set.mem_sep_iff

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