Theorems · Inductive type · combinatorics

IsCorner

{G : Type u_1} → [AddCommMonoid G] → Set (G × G) → G → G → G → G → Prop

A corner of a set A in an abelian group is a triple of points of the form (x, y), (x + d, y), (x, y + d). It is nontrivial if d ≠ 0. Here we define it as triples (x₁, y₁), (x₂, y₁), (x₁, y₂) where x₁ + y₂ = x₂ + y₁ in order for the definition to make sense in commutative monoids, the motivating example being ℕ.

Defined in

Mathlib.Combinatorics.Additive.Corner.Defs

Cited by

16 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

AddCommMonoid