Theorems · Theorem · group theory

sdiv_smul_eq_sdiv_div

∀ {G : Type u_1} {P : Type u_2} [inst : Group G] [T : Torsor G P] (p₁ p₂ : P) (g : G), p₁ /ₛ g • p₂ = (p₁ /ₛ p₂) / g

Dividing by the result of multiplying with a group element produces the same result as dividing the points and dividing by that group element.

Defined in

Mathlib.Algebra.Torsor.Defs

Cited by

6 results in Mathlib

Foundations

Depth 13 from the axioms · uses propext

Assumes

GroupTorsor