Commit 2025-02-27 21:16 20811cf5

View on Github →

chore: split Mathlib.Algebra.AddTorsor into Defs/Basic (#22310) Preliminary to splitting the long file Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.

Estimated changes

added theorem Equiv.constVAdd_add
added theorem Equiv.constVAdd_zero
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 vsub_left_cancel
added theorem vsub_left_cancel_iff
added theorem vsub_left_injective
added theorem vsub_right_cancel
added theorem vsub_right_cancel_iff
added theorem vsub_right_injective
added theorem vsub_sub_vsub_comm
added theorem vsub_vadd_comm
deleted def Equiv.constVAddHom
deleted theorem Equiv.constVAdd_add
deleted theorem Equiv.constVAdd_zero
deleted theorem Prod.fst_vadd
deleted theorem Prod.fst_vsub
deleted theorem Prod.mk_vadd_mk
deleted theorem Prod.mk_vsub_mk
deleted theorem Prod.snd_vadd
deleted theorem Prod.snd_vsub
deleted theorem Set.singleton_vsub_self
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
deleted theorem div_mul_cancel
deleted theorem div_self'
deleted theorem inv_eq_one_div
deleted theorem mul_div_assoc
deleted theorem mul_div_cancel_right
deleted theorem mul_left_inj
deleted theorem mul_left_injective
deleted theorem mul_ne_mul_left
deleted theorem mul_ne_mul_right
deleted theorem mul_right_inj
deleted theorem mul_right_injective
deleted theorem one_div
added theorem div_mul_cancel
added theorem div_self'
added theorem inv_eq_one_div
added theorem mul_div_assoc
added theorem mul_div_cancel_right
added theorem mul_left_inj
added theorem mul_left_injective
added theorem mul_ne_mul_left
added theorem mul_ne_mul_right
added theorem mul_right_inj
added theorem mul_right_injective
added theorem one_div
deleted theorem Function.Injective.beq_eq
deleted theorem Function.Injective.eq_iff
deleted theorem Function.Injective.ne
deleted theorem Function.Injective.ne_iff
added theorem Function.Injective.ne