Theorems · Theorem · group theory

UniqueAdd.addHom_preimage

∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] (f : G →ₙ+ H) (hf : Function.Injective ⇑f) (a0 b0 : G)
  {A B : Finset H}, UniqueAdd A B (f a0) (f b0) → UniqueAdd (A.preimage ⇑f ⋯) (B.preimage ⇑f ⋯) a0 b0

UniqueAdd is preserved by inverse images under injective, additive maps.

Defined in

Mathlib.Algebra.Group.UniqueProds.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddAdd