Structures · Algebra
Torsor
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
- Shape
- 2 explicit arguments · adds nonempty, sdiv_smul', smul_sdiv'
Extends2
Extended by1
Forgetful instances
Concrete types that are instances1
- Prod
How is a type an instance?
Loading the hierarchy index…
Assumed by80
- smul_sdiv_assoc
- sdiv_self
- sdiv_smul_eq_sdiv_div
- sdiv_smul
- smul_right_cancel
- smul_sdiv
- sdiv_mul_sdiv_cancel
- sdiv_eq_one_iff_eq
- Equiv.smulConst
- Equiv.constSMul
- inv_sdiv_eq_sdiv_rev
- sdiv_right_cancel
- Homeomorph.constSDiv
- Homeomorph.smulConst
- Filter.Tendsto.sdiv
- Equiv.constSDiv
- sdiv_left_cancel
- sdiv_smul_comm
- smul_sdiv_smul_comm
- eq_of_sdiv_eq_one
- Torsor.smul_sdiv'
- eq_smul_iff_sdiv_eq
- sdiv_div_sdiv_cancel_right
- Torsor.sdiv_smul'
- smul_eq_smul_iff_inv_mul_eq_sdiv
- ContinuousWithinAt.sdiv
- smul_sdiv_smul_cancel_left
- sdiv_div_sdiv_cancel_left
- sdiv_ne_one
- sdiv_left_cancel_iff
- Equiv.coe_constSMul
- Pi.sdiv_def
- Set.one_mem_sdiv_iff
- Function.Surjective.torsor
- Pi.instTorsor
- Torsor.nonempty
- Prod.mk_sdiv_mk
- div_mul_sdiv_comm
- Torsor.toSDiv
- smul_eq_smul_iff_div_eq_sdiv
- Continuous.sdiv
- smul_right_injective'
- Prod.mk_smul_mk
- Equiv.constSMul_one
- Equiv.coe_constSDiv_symm
- sdiv_right_injective
- Homeomorph.smulConst_apply
- Homeomorph.constSDiv_apply
- Set.singleton_sdiv_self
- Equiv.coe_constSDiv