Theorems · Theorem · ring theory

IsInvariantSubring.smul_mem

∀ {M : Type u_1} {R : Type u_2} {inst : Monoid M} {inst_1 : Ring R} {inst_2 : MulSemiringAction M R} {S : Subring R}
  [self : IsInvariantSubring M S] (m : M) {x : R}, x ∈ S → m • x ∈ S

Defined in

Mathlib.Algebra.Ring.Action.Invariant

Cited by

0 results in Mathlib

Foundations

Depth 19 from the axioms · uses propext

Assumes

IsInvariantSubring