Theorems · Inductive type · group theory

AddTorsor

(G : outParam (Type u_1)) → Type u_2 → [AddGroup G] → Type (max u_1 u_2)

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

Cited by

1,657 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 3 definitions · uses no axioms

Assumes

AddGroup