Mathlib Map

Theorems · Theorem · group theory

Prod.mk_sdiv_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'] (p₁ p₂ : P) (p₁' p₂' : P'),
  (p₁, p₁') /ₛ (p₂, p₂') = (p₁ /ₛ p₂, p₁' /ₛ 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 6238GroupSDiv.sdiv · cited by 79SDiv.sdivTorsor · cited by 65TorsorProd.mk_sdiv_mkCITED BYCITES

Cites3

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
  • SDiv.sdivstatement · cited by 79
  • Torsorstatement and proof · cited by 65

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.