Theorems · Theorem · group theory

AddSubmonoid.closure_prod

∀ {N : Type u_2} [inst : AddZeroClass N] {M : Type u_5} [inst_1 : AddZeroClass M] {s : Set M} {t : Set N},
  0 ∈ s → 0 ∈ t → AddSubmonoid.closure (s ×ˢ t) = (AddSubmonoid.closure s).prod (AddSubmonoid.closure t)

Defined in

Mathlib.Algebra.Group.Submonoid.Operations

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddZeroClassAddZeroClass