Theorems · Definition · group theory

UniqueAdd

{G : Type u_1} → [Add G] → Finset G → Finset G → G → G → Prop

Let G be a Type with addition, let A B : Finset G be finite subsets and let a0 b0 : G be two elements. UniqueAdd A B a0 b0 asserts a0 + b0 can be written in at most one way as a sum of an element from A and an element from B.

Defined in

Mathlib.Algebra.Group.UniqueProds.Basic

Cited by

27 results in Mathlib

Foundations

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

Assumes

Add