Theorems · Theorem · group theory
smul_eq_smul_iff_inv_mul_eq_sdiv
∀ {G : Type u_1} {P : Type u_2} [inst : Group G] [T : Torsor G P] {v₁ v₂ : G} {p₁ p₂ : P},
v₁ • p₁ = v₂ • p₂ ↔ v₁⁻¹ * v₂ = p₁ /ₛ p₂- Defined in
- Mathlib.Algebra.Torsor.Defs
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 13 from the axioms · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
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
- inv_mul_cancel_leftproof · cited by 88
- SDiv.sdivstatement and proof · cited by 79
- Torsorstatement and proof · cited by 65
- mul_right_injproof · cited by 11
- smul_sdiv_assocproof · cited by 7
- eq_smul_iff_sdiv_eqproof · cited by 1
Cited by1
Results whose statement or proof uses this declaration.
- smul_eq_smul_iff_div_eq_sdivproof · cited by 0