Mathlib Map

Theorems · Definition · group theory

Equiv.constSMul

{G : Type u_1} → (P : Type u_2) → [inst : Group G] → [Torsor G P] → G → Equiv.Perm P

The permutation given by p ↦ v • p.

Defined in
Mathlib.Algebra.Torsor.Defs
Cited by
3 results in Mathlib
Foundations
Depth 10 from the axioms · uses propext
Assumes
GroupTorsor
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Equiv.constSMulHom · cited by 0Equiv.constSMulHomEquiv.constSMul_mul · cited by 0Equiv.constSMul_mulEquiv.constSMul_one · cited by 0Equiv.constSMul_oneEquiv.coe_constSMul · cited by 0Equiv.coe_constSMulGroup · cited by 6238GroupEquiv.Perm · cited by 1375Equiv.PermTorsor · cited by 65TorsorEquiv.constSMulCITED 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
  • Equiv.Permstatement · cited by 1,375
  • Torsorstatement and proof · cited by 65

Cited by4

Results whose statement or proof uses this declaration.