Theorems · Theorem · ring theory

Subsemiring.smul_mem_pointwise_smul

∀ {M : Type u_1} {R : Type u_2} [inst : Monoid M] [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R] (m : M) (r : R)
  (S : Subsemiring R), r ∈ S → m • r ∈ m • S

Defined in: Mathlib.Algebra.Ring.Subsemiring.Pointwise
Cited by: 0 results in Mathlib
Foundations: Depth 23 from the axioms · uses propext, Quot.sound
Assumes: Monoid Semiring MulSemiringAction

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Semiringstatement and proof · cited by 13,802
Monoidstatement and proof · cited by 3,887
Subsemiringstatement and proof · cited by 456
MulSemiringActionstatement and proof · cited by 423
Set.smul_mem_smul_setproof · cited by 39
Subsemiring.pointwiseMulActionstatement · cited by 22

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.