Theorems · Definition · group theory

UniqueMul

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

Let G be a Type with multiplication, let A B : Finset G be finite subsets and let a0 b0 : G be two elements. UniqueMul A B a0 b0 asserts a0 * b0 can be written in at most one way as a product of an element of A and an element of B.

Defined in

Mathlib.Algebra.Group.UniqueProds.Basic

Cited by

28 results in Mathlib

Foundations

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

Assumes

Mul