Mathlib Map

Theorems · Theorem · group theory

Prod.mk_smul_mk

∀ {G : Type u_1} {G' : Type u_2} {P : Type u_3} {P' : Type u_4} [inst : Group G] [inst_1 : Group G']
  [inst_2 : Torsor G P] [inst_3 : Torsor G' P'] (v : G) (v' : G') (p : P) (p' : P'),
  (v, v') • (p, p') = (v • p, v' • p')
Defined in
Mathlib.Algebra.Torsor.Basic
Cited by
0 results in Mathlib
Foundations
Depth 17 from the axioms · uses propext, Quot.sound
Assumes
GroupGroupTorsorTorsor
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Group · cited by 6238GroupTorsor · cited by 65TorsorProd.mk_smul_mkCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Groupstatement and proof · cited by 6,238
  • Torsorstatement and proof · cited by 65

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.