Commit 2023-02-07 09:23 e6e8b4d5

View on Github →

feat: port Algebra.AddTorsor (#1542)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/AddTorsor.lean

added theorem AddTorsor.subsingleton_iff

added theorem Equiv.coe_constVAdd

added theorem Equiv.coe_constVSub

added theorem Equiv.coe_constVSub_symm

added theorem Equiv.coe_vaddConst

added theorem Equiv.coe_vaddConst_symm

added def Equiv.constVAdd

added def Equiv.constVAddHom

added theorem Equiv.constVAdd_add

added theorem Equiv.constVAdd_zero

added def Equiv.constVSub

added theorem Equiv.injective_pointReflection_left_of_injective_bit0

added def Equiv.pointReflection

added theorem Equiv.pointReflection_apply

added theorem Equiv.pointReflection_fixed_iff_of_injective_bit0

added theorem Equiv.pointReflection_involutive

added theorem Equiv.pointReflection_self

added theorem Equiv.pointReflection_symm

added def Equiv.vaddConst

added theorem Prod.fst_vadd

added theorem Prod.fst_vsub

added theorem Prod.mk_vadd_mk

added theorem Prod.mk_vsub_mk

added theorem Prod.snd_vadd

added theorem Prod.snd_vsub

added theorem Set.singleton_vsub_self

added theorem eq_of_vsub_eq_zero

added theorem eq_vadd_iff_vsub_eq

added theorem neg_vsub_eq_vsub_rev

added theorem vadd_eq_vadd_iff_neg_add_eq_vsub

added theorem vadd_eq_vadd_iff_sub_eq_vsub

added theorem vadd_right_cancel

added theorem vadd_right_cancel_iff

added theorem vadd_right_injective

added theorem vadd_vsub

added theorem vadd_vsub_assoc

added theorem vadd_vsub_eq_sub_vsub

added theorem vadd_vsub_vadd_cancel_left

added theorem vadd_vsub_vadd_cancel_right

added theorem vsub_add_vsub_cancel

added theorem vsub_eq_sub

added theorem vsub_eq_zero_iff_eq

added theorem vsub_left_cancel

added theorem vsub_left_cancel_iff

added theorem vsub_left_injective

added theorem vsub_ne_zero

added theorem vsub_right_cancel

added theorem vsub_right_cancel_iff

added theorem vsub_right_injective

added theorem vsub_self

added theorem vsub_sub_vsub_cancel_left

added theorem vsub_sub_vsub_cancel_right

added theorem vsub_sub_vsub_comm

added theorem vsub_vadd

added theorem vsub_vadd_comm

added theorem vsub_vadd_eq_vsub_sub