Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2021-04-02 21:56
267e6608
View on Github →
refactor(algebra/add_torsor): use
to_additive
for
add_action
(
#6914
)
Estimated changes
Modified
src/algebra/add_torsor.lean
deleted
theorem
vadd_assoc
deleted
theorem
vadd_comm
deleted
theorem
vadd_eq_add
deleted
theorem
vadd_left_cancel
deleted
theorem
vadd_left_cancel_iff
deleted
theorem
vadd_left_injective
deleted
theorem
zero_vadd
Modified
src/algebra/group/to_additive.lean
Modified
src/algebra/module/prod.lean
deleted
theorem
prod.smul_fst
deleted
theorem
prod.smul_mk
deleted
theorem
prod.smul_snd
Modified
src/group_theory/group_action/defs.lean
modified
def
const_smul_hom
modified
theorem
const_smul_hom_apply
modified
def
distrib_mul_action.comp_hom
modified
theorem
ite_smul
modified
def
mul_action.comp_hom
modified
def
mul_action.to_fun
modified
theorem
mul_action.to_fun_apply
modified
theorem
one_smul
modified
theorem
smul_add
modified
theorem
smul_comm_class.symm
modified
theorem
smul_eq_mul
modified
theorem
smul_ite
modified
theorem
smul_neg
modified
theorem
smul_smul
modified
theorem
smul_sub
modified
theorem
smul_zero
Modified
src/group_theory/group_action/group.lean
added
def
add_units.vadd_perm_hom
modified
theorem
eq_inv_smul_iff
modified
theorem
inv_smul_eq_iff
modified
theorem
inv_smul_smul
modified
theorem
is_unit.smul_left_cancel
modified
theorem
smul_inv_smul
added
theorem
smul_left_cancel
added
theorem
smul_left_cancel_iff
modified
theorem
units.inv_smul_smul
modified
theorem
units.smul_eq_iff_eq_inv_smul
modified
theorem
units.smul_inv_smul
modified
theorem
units.smul_left_cancel
added
def
units.smul_perm
Created
src/group_theory/group_action/prod.lean
added
theorem
prod.smul_fst
added
theorem
prod.smul_mk
added
theorem
prod.smul_snd
Modified
src/linear_algebra/affine_space/affine_equiv.lean
Modified
src/linear_algebra/affine_space/affine_map.lean
Modified
src/linear_algebra/affine_space/affine_subspace.lean
Modified
src/linear_algebra/affine_space/combination.lean
Modified
src/linear_algebra/affine_space/finite_dimensional.lean
Modified
src/linear_algebra/affine_space/midpoint.lean