Theorems · Theorem · commutative algebra

AddSubmonoid.smul_le

∀ {R : Type u_2} {A : Type u_3} [inst : AddMonoid R] [inst_1 : AddMonoid A] [inst_2 : DistribSMul R A]
  {M : AddSubmonoid R} {N P : AddSubmonoid A}, M • N ≤ P ↔ ∀ m ∈ M, ∀ n ∈ N, m • n ∈ P

Defined in

Mathlib.Algebra.Ring.Submonoid.Pointwise

Cited by

8 results in Mathlib

Foundations

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

Assumes

AddMonoidAddMonoidDistribSMul