Mathlib Map

Theorems · Definition · group theory

Function.Surjective.mulAction

{M : Type u_1} →
  {α : Type u_5} →
    {β : Type u_6} →
      [inst : Monoid M] →
        [inst_1 : MulAction M α] →
          [inst_2 : SMul M β] →
            (f : α → β) → Function.Surjective f → (∀ (c : M) (x : α), f (c • x) = c • f x) → MulAction M β

Pushforward a multiplicative action along a surjective map respecting •. See note [reducible non-instances].

Defined in
Mathlib.Algebra.Group.Action.Defs
Cited by
0 results in Mathlib
Foundations
Depth 9 from the axioms · uses propext, Quot.sound
Assumes
MonoidMulActionSMul
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Function.Surjective.mulActionWithZero · cited by 0Surjective.mulActionWithZ…Function.Surjective.mulDistribMulAction · cited by 0Surjective.mulDistribMulA…Function.Surjective.torsor · cited by 0Surjective.torsorFunction.Surjective.distribMulAction · cited by 0Surjective.distribMulActi…Monoid · cited by 3887MonoidMulAction · cited by 1294MulActionSurjective.mulActionCITED BYCITES

Cites2

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

  • Monoidstatement and proof · cited by 3,887
  • MulActionstatement and proof · cited by 1,294

Cited by4

Results whose statement or proof uses this declaration.