Mathlib Map

Theorems · Definition · combinatorics

IsCornerFree

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

A corner-free set in an abelian group is a set containing no non-trivial corner.

Defined in
Mathlib.Combinatorics.Additive.Corner.Defs
Cited by
10 results in Mathlib
Foundations
Depth 2 from the axioms · uses no axioms
Assumes
AddCommMonoid
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Set.Subsingleton.isCornerFree · cited by 2Subsingleton.isCornerFreecorners_theorem · cited by 2corners_theoremIsCornerFree.of_image · cited by 1IsCornerFree.of_imageisCornerFree_iff · cited by 1isCornerFree_iffisCornerFree_image · cited by 1isCornerFree_imageIsCornerFree.image · cited by 0IsCornerFree.imagecorners_theorem_nat · cited by 0corners_theorem_natisCornerFree_empty · cited by 0isCornerFree_emptyisCornerFree_singleton · cited by 0isCornerFree_singletonIsCornerFree.mono · cited by 0IsCornerFree.monoSet · cited by 53352SetAddCommMonoid · cited by 12281AddCommMonoidIsCorner · cited by 16IsCornerIsCornerFreeCITED BYCITES

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Setstatement and proof · cited by 53,352
  • AddCommMonoidstatement and proof · cited by 12,281
  • IsCornerproof · cited by 16

Cited by10

Results whose statement or proof uses this declaration.