Theorems · Theorem · group theory

AddSubmonoid.prod_le_iff

∀ {N : Type u_2} [inst : AddZeroClass N] {M : Type u_5} [inst_1 : AddZeroClass M] {s : AddSubmonoid M}
  {t : AddSubmonoid N} {u : AddSubmonoid (M × N)},
  s.prod t ≤ u ↔ AddSubmonoid.map (AddMonoidHom.inl M N) s ≤ u ∧ AddSubmonoid.map (AddMonoidHom.inr M N) t ≤ u

Defined in

Mathlib.Algebra.Group.Submonoid.Operations

Cited by

5 results in Mathlib

Foundations

Depth 24 from the axioms · uses propext, Quot.sound

Assumes

AddZeroClassAddZeroClass