Mathlib Map

Theorems · Definition · group theory

Equiv.constSDiv

{G : Type u_1} → {P : Type u_2} → [inst : Group G] → [Torsor G P] → P → P ≃ G

p' ↦ p /ₛ p' as an equivalence.

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

Around this declaration

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

Homeomorph.constSDiv · cited by 2Homeomorph.constSDivEquiv.coe_constSDiv · cited by 0Equiv.coe_constSDivEquiv.coe_constSDiv_symm · cited by 0Equiv.coe_constSDiv_symmEquiv · cited by 8337EquivGroup · cited by 6238GroupSDiv.sdiv · cited by 79SDiv.sdivTorsor · cited by 65TorsorEquiv.constSDivCITED BYCITES

Cites4

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

  • Equivstatement · cited by 8,337
  • Groupstatement and proof · cited by 6,238
  • SDiv.sdivproof · cited by 79
  • Torsorstatement and proof · cited by 65

Cited by3

Results whose statement or proof uses this declaration.