Structures · Algebra
AddTorsor
An AddTorsor G P gives a structure to the nonempty type P,
acted on by an AddGroup G with a transitive and free action given
by the +ᵥ operation and a corresponding subtraction given by the
-ᵥ operation. In the case of a vector space, it is an affine
space.
- Defined in
- Mathlib.Algebra.Torsor.Defs
- Shape
- 2 explicit arguments · adds nonempty, vsub_vadd', vadd_vsub'
Extends2
Extended by2
Forgetful instances
Concrete types that are instances4
- ContinuousAffineMap
- AffineMap
- Subtype
- Prod
How is a type an instance?
Loading the hierarchy index…
Assumed by1,832
- affineSpan
- Affine.Simplex.points
- AffineSubspace.direction
- AffineMap.lineMap
- Wbtw
- Finset.affineCombination
- slope
- AffineIndependent
- midpoint
- vectorSpan
- Sbtw
- AffineMap.linear
- Affine.Simplex.faceOpposite
- neg_vsub_eq_vsub_rev
- Collinear
- AffineSubspace.map
- Affine.Triangle
- vsub_self
- AffineEquiv.toAffineMap
- vsub_vadd
- vadd_vsub
- AffineSubspace.SOppSide
- AffineSubspace.SSameSide
- AffineEquiv.symm
- AffineSubspace.WSameSide
- AffineMap.homothety
- Finset.weightedVSub
- AffineSubspace.WOppSide
- direction_affineSpan
- Finset.centroid
- Affine.Simplex.reindex
- Affine.Simplex.independent
- ContinuousAffineMap.contLinear
- vsub_eq_zero_iff_eq
- Affine.Simplex.map
- Finset.weightedVSubOfPoint
- vsub_add_vsub_cancel
- AffineMap.lineMap_apply_zero
- vadd_vsub_assoc
- Finset.weightedVSubOfPoint_apply
- Affine.Simplex.faceOppositeCentroid
- vsub_sub_vsub_cancel_right
- vsub_ne_zero
- Affine.Simplex.centroid
- AffineSubspace.inclusion
- AffineEquiv.toEquiv
- ContinuousAffineEquiv.toAffineEquiv
- AffineMap.lineMap_apply_one
- Sbtw.wbtw
- Affine.Simplex.face