Mathlib Map

Theorems · Theorem · group theory

Submonoid.smul_def

∀ {M' : Type u_1} {α : Type u_2} [inst : MulOneClass M'] [inst_1 : SMul M' α] {S : Submonoid M'} (g : ↥S) (a : α),
  g • a = ↑g • a
Defined in
Mathlib.Algebra.Group.Submonoid.MulAction
Cited by
42 results in Mathlib
Foundations
Depth 12 from the axioms · uses no axioms
Assumes
MulOneClassSMul
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

IsIntegralClosure.isLocalization · cited by 13IsIntegralClosure.isLocal…IsIntegral.exists_multiple_integral_of_isLocalization · cited by 7IsIntegral.exists_multipl…IsLocalizedModule.mk'_cancel' · cited by 6IsLocalizedModule.mk'_can…OreLocalization.expand · cited by 4OreLocalization.expandIsLocalizedModule.mk'_eq_iff · cited by 4IsLocalizedModule.mk'_eq_…span_eq_top_of_isLocalizedModule · cited by 3span_eq_top_of_isLocalize…IsLocalizedModule.mk'_smul_mk' · cited by 3IsLocalizedModule.mk'_smu…IsLocalizedModule.exist_integer_multiples · cited by 3IsLocalizedModule.exist_i…AlgebraicGeometry.StructureSheaf.Localizations.comapFun_mk · cited by 3Localizations.comapFun_mkIsLocalizedModule.fromLocalizedModule.inj · cited by 2fromLocalizedModule.injIsLocalizedModule.iso_symm_apply' · cited by 2IsLocalizedModule.iso_sym…Module.Finite.of_localizationSpan_finite' · cited by 2Finite.of_localizationSpa…IsLocalization.exists_smul_mem_of_mem_adjoin · cited by 2IsLocalization.exists_smu…Rep.indToCoindAux_mul_snd · cited by 2Rep.indToCoindAux_mul_sndIsLocalizedModule.mk_eq_mk' · cited by 2IsLocalizedModule.mk_eq_m…Submonoid · cited by 3086SubmonoidMulOneClass · cited by 1018MulOneClassSubmonoid.smul_defCITED BYCITES

Cites2

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

Cited by42

Results whose statement or proof uses this declaration.