Mathlib Map

Theorems · Theorem · group theory

MulAction.subgroup_smul_def

∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {H : Subgroup G} (a : ↥H) (b : α),
  a • b = ↑a • b
Defined in
Mathlib.GroupTheory.GroupAction.Defs
Cited by
3 results in Mathlib
Foundations
Depth 22 from the axioms · uses propext
Assumes
GroupMulAction
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

MulAction.orbitRel.Quotient.mem_subgroup_orbit_iff · cited by 2Quotient.mem_subgroup_orb…IsGaloisGroup.map_quotientMk' · cited by 1IsGaloisGroup.map_quotien…MulAction.mem_subgroup_orbit_iff · cited by 0MulAction.mem_subgroup_or…Group · cited by 6238GroupSubgroup · cited by 3593SubgroupMulAction · cited by 1294MulActionMulAction.subgroup_smul_defCITED BYCITES

Cites3

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

  • Groupstatement and proof · cited by 6,238
  • Subgroupstatement and proof · cited by 3,593
  • MulActionstatement and proof · cited by 1,294

Cited by3

Results whose statement or proof uses this declaration.