Mathlib Map

Theorems · Definition · group theory

Equiv.mulAction

(M : Type u_1) → {α : Type u_4} → {β : Type u_5} → [inst : Monoid M] → α ≃ β → [MulAction M β] → MulAction M α

Transfer MulAction across an Equiv

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

Around this declaration

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

KaehlerDifferential.mulActionBaseChange · cited by 3KaehlerDifferential.mulAc…KaehlerDifferential.moduleBaseChange · cited by 0KaehlerDifferential.modul…Equiv.distribMulAction · cited by 0Equiv.distribMulActionEquiv.mulActionWithZero · cited by 0Equiv.mulActionWithZeroEquiv.mulDistribMulAction · cited by 0Equiv.mulDistribMulActionEquiv · cited by 8337EquivMonoid · cited by 3887MonoidMulAction · cited by 1294MulActionEquiv.smul · cited by 7Equiv.smulEquiv.mulActionCITED BYCITES

Cites4

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

  • Equivstatement and proof · cited by 8,337
  • Monoidstatement and proof · cited by 3,887
  • MulActionstatement and proof · cited by 1,294
  • Equiv.smulproof · cited by 7

Cited by5

Results whose statement or proof uses this declaration.