Theorems · Theorem · group theory

AddSubmonoid.pi_le_iff

∀ {η : Type u_1} {f : η → Type u_2} [inst : (i : η) → AddZeroClass (f i)] [Finite η] [inst_2 : DecidableEq η]
  {H : (i : η) → AddSubmonoid (f i)} {J : AddSubmonoid ((i : η) → f i)},
  AddSubmonoid.pi Set.univ H ≤ J ↔ ∀ (i : η), AddSubmonoid.map (AddMonoidHom.single f i) (H i) ≤ J

For finite index types, the Submonoid.pi is generated by the embeddings of the additive monoids.

Defined in

Mathlib.Algebra.Group.Submonoid.Finite

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddZeroClassFiniteDecidableEq