Theorems · Theorem · group theory

SetLike.mk_smul_mk

∀ {S : Type u'} {R : Type u} {M : Type v} [inst : SMul R M] [inst_1 : SetLike S M] [hS : SMulMemClass S R M] (s : S)
  (r : R) (x : M) (hx : x ∈ s), r • ⟨x, hx⟩ = ⟨r • x, ⋯⟩

Defined in: Mathlib.GroupTheory.GroupAction.SubMulAction
Cited by: 2 results in Mathlib
Foundations: Depth 8 from the axioms · uses no axioms
Assumes: SMul SetLike SMulMemClass

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites3

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

SetLikestatement and proof · cited by 1,084
SMulMemClassstatement and proof · cited by 77
SMulMemClass.smul_memstatement · cited by 55

Cited by2

Results whose statement or proof uses this declaration.

LieAlgebra.Basis.baseSupp_apply_smul_eproof · cited by 3
Module.Baer.of_divisibleproof · cited by 1