Theorems · Inductive type · group theory
Torsor
(G : outParam (Type u_1)) → Type u_2 → [Group G] → Type (max u_1 u_2)
A Torsor G P gives a structure to the nonempty type P,
acted on by a Group G with a transitive and free action given
by the • operation and a corresponding division given by the
/ₛ operation.
- Defined in
- Mathlib.Algebra.Torsor.Defs
- Cited by
- 65 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- Group
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Groupstatement · cited by 6,238
Cited by82
Results whose statement or proof uses this declaration.
- IsTopologicalTorsorstatement · cited by 11
- smul_sdiv_assocstatement and proof · cited by 7
- sdiv_selfstatement and proof · cited by 6
- sdiv_smulstatement and proof · cited by 6
- sdiv_smul_eq_sdiv_divstatement and proof · cited by 6
- smul_right_cancelstatement and proof · cited by 5
- sdiv_mul_sdiv_cancelstatement and proof · cited by 4
- smul_sdivstatement and proof · cited by 4
- sdiv_eq_one_iff_eqstatement and proof · cited by 3
- inv_sdiv_eq_sdiv_revstatement and proof · cited by 3
- Equiv.smulConststatement and proof · cited by 3
- Equiv.constSMulstatement and proof · cited by 3