Theorems · Theorem · combinatorics

Finset.HasMulAntidiagonal.mem_mulAntidiagonal_ofAdd_iff_toAdd_mem_antidiagonal

∀ {A : Type u_2} [inst : AddMonoid A] [inst_1 : Finset.HasAntidiagonal A] {a : A}
  {p : Multiplicative A × Multiplicative A},
  p ∈ Finset.HasMulAntidiagonal.mulAntidiagonal (Multiplicative.ofAdd a) ↔
    (Multiplicative.toAdd p.1, Multiplicative.toAdd p.2) ∈ Finset.HasAntidiagonal.antidiagonal a

Defined in

Mathlib.Algebra.Order.Antidiag.Prod

Cited by

0 results in Mathlib

Foundations

Depth 58 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddMonoidFinset.HasAntidiagonal