Commit 2026-06-12 01:48 fef49b73

View on Github →

feat(Algebra): multiplicative torsors (#38896) Introduce a class Torsor for torsors of multiplicative groups, as a multiplicative counterpart to the existing AddTorsor for torsors of additive groups.

Estimated changes

added theorem Equiv.constSMul_mul
added theorem Equiv.constSMul_one
modified def Equiv.constVAddHom
deleted theorem Equiv.constVAdd_add
deleted theorem Equiv.constVAdd_zero
added theorem Pi.sdiv_apply
added theorem Pi.sdiv_def
deleted theorem Pi.vsub_apply
deleted theorem Pi.vsub_def
added theorem Prod.fst_sdiv
added theorem Prod.fst_smul
deleted theorem Prod.fst_vadd
deleted theorem Prod.fst_vsub
added theorem Prod.mk_sdiv_mk
added theorem Prod.mk_smul_mk
deleted theorem Prod.mk_vadd_mk
deleted theorem Prod.mk_vsub_mk
added theorem Prod.snd_sdiv
added theorem Prod.snd_smul
deleted theorem Prod.snd_vadd
deleted theorem Prod.snd_vsub
deleted theorem Set.singleton_vsub_self
added theorem div_mul_sdiv_comm
added theorem sdiv_div_sdiv_comm
added theorem sdiv_left_cancel
added theorem sdiv_left_cancel_iff
added theorem sdiv_left_injective
added theorem sdiv_right_cancel
added theorem sdiv_right_cancel_iff
added theorem sdiv_right_injective
added theorem sdiv_smul_comm
added theorem smul_sdiv_smul_comm
deleted theorem sub_add_vsub_comm
deleted theorem vadd_vsub_vadd_comm
deleted theorem vsub_left_cancel
deleted theorem vsub_left_cancel_iff
deleted theorem vsub_left_injective
deleted theorem vsub_right_cancel
deleted theorem vsub_right_cancel_iff
deleted theorem vsub_right_injective
deleted theorem vsub_sub_vsub_cancel_left
deleted theorem vsub_sub_vsub_comm
deleted theorem vsub_vadd_comm
added theorem Equiv.coe_constSDiv
added theorem Equiv.coe_constSMul
deleted theorem Equiv.coe_constVAdd
deleted theorem Equiv.coe_constVSub
deleted theorem Equiv.coe_constVSub_symm
added theorem Equiv.coe_smulConst
deleted theorem Equiv.coe_vaddConst
deleted theorem Equiv.coe_vaddConst_symm
added def Equiv.constSDiv
added def Equiv.constSMul
deleted def Equiv.constVAdd
deleted def Equiv.constVSub
added def Equiv.smulConst
deleted def Equiv.vaddConst
added theorem eq_of_sdiv_eq_one
deleted theorem eq_of_vsub_eq_zero
added theorem eq_smul_iff_sdiv_eq
deleted theorem eq_vadd_iff_vsub_eq
added theorem inv_sdiv_eq_sdiv_rev
deleted theorem neg_vsub_eq_vsub_rev
added theorem sdiv_eq_div
added theorem sdiv_eq_one_iff_eq
added theorem sdiv_mul_sdiv_cancel
added theorem sdiv_ne_one
added theorem sdiv_self
added theorem sdiv_smul
added theorem sdiv_smul_eq_sdiv_div
added theorem smul_right_cancel
added theorem smul_right_cancel_iff
added theorem smul_right_injective'
added theorem smul_sdiv
added theorem smul_sdiv_assoc
added theorem smul_sdiv_eq_div_sdiv
deleted theorem vadd_right_cancel
deleted theorem vadd_right_cancel_iff
deleted theorem vadd_right_injective
deleted theorem vadd_vsub
deleted theorem vadd_vsub_assoc
deleted theorem vadd_vsub_eq_sub_vsub
deleted theorem vsub_add_vsub_cancel
deleted theorem vsub_eq_sub
deleted theorem vsub_eq_zero_iff_eq
deleted theorem vsub_ne_zero
deleted theorem vsub_self
deleted theorem vsub_vadd
deleted theorem vsub_vadd_eq_vsub_sub
deleted theorem Set.Nonempty.of_vsub_left
added theorem Set.Nonempty.sdiv
deleted theorem Set.Nonempty.vsub
added theorem Set.empty_sdiv
deleted theorem Set.empty_vsub
added theorem Set.image2_sdiv
deleted theorem Set.image2_vsub
added theorem Set.image_sdiv_prod
deleted theorem Set.image_vsub_prod
added theorem Set.inter_sdiv_subset
deleted theorem Set.inter_vsub_subset
added theorem Set.mem_sdiv
deleted theorem Set.mem_vsub
added theorem Set.sdiv_empty
added theorem Set.sdiv_eq_empty
added theorem Set.sdiv_inter_subset
added theorem Set.sdiv_mem_sdiv
added theorem Set.sdiv_nonempty
added theorem Set.sdiv_self_mono
added theorem Set.sdiv_singleton
added theorem Set.sdiv_subset_iff
added theorem Set.sdiv_subset_sdiv
added theorem Set.sdiv_union
added theorem Set.singleton_sdiv
deleted theorem Set.singleton_vsub
added theorem Set.union_sdiv
deleted theorem Set.union_vsub
deleted theorem Set.vsub_empty
deleted theorem Set.vsub_eq_empty
deleted theorem Set.vsub_inter_subset
deleted theorem Set.vsub_mem_vsub
deleted theorem Set.vsub_nonempty
deleted theorem Set.vsub_self_mono
deleted theorem Set.vsub_singleton
deleted theorem Set.vsub_subset_iff
deleted theorem Set.vsub_subset_vsub
deleted theorem Set.vsub_subset_vsub_left
deleted theorem Set.vsub_union