Mathlib Changelog
Changelog
About
Github
Commit
2021-09-24 11:04
48883dcd
View on Github →
chore(algebra/basic): split out facts about lmul (
#9300
)
Estimated changes
Modified
src/algebra/algebra/basic.lean
deleted
theorem
algebra.commute_lmul_left_right
deleted
def
algebra.lmul'
deleted
theorem
algebra.lmul'_apply
deleted
def
algebra.lmul
deleted
theorem
algebra.lmul_apply
deleted
theorem
algebra.lmul_injective
deleted
def
algebra.lmul_left
deleted
theorem
algebra.lmul_left_apply
deleted
theorem
algebra.lmul_left_eq_zero_iff
deleted
theorem
algebra.lmul_left_injective
deleted
theorem
algebra.lmul_left_mul
deleted
theorem
algebra.lmul_left_one
deleted
def
algebra.lmul_left_right
deleted
theorem
algebra.lmul_left_right_apply
deleted
theorem
algebra.lmul_left_zero_eq_zero
deleted
def
algebra.lmul_right
deleted
theorem
algebra.lmul_right_apply
deleted
theorem
algebra.lmul_right_eq_zero_iff
deleted
theorem
algebra.lmul_right_injective
deleted
theorem
algebra.lmul_right_mul
deleted
theorem
algebra.lmul_right_one
deleted
theorem
algebra.lmul_right_zero_eq_zero
deleted
theorem
algebra.pow_lmul_left
deleted
theorem
algebra.pow_lmul_right
Created
src/algebra/algebra/bilinear.lean
added
theorem
algebra.commute_lmul_left_right
added
def
algebra.lmul'
added
theorem
algebra.lmul'_apply
added
def
algebra.lmul
added
theorem
algebra.lmul_apply
added
theorem
algebra.lmul_injective
added
def
algebra.lmul_left
added
theorem
algebra.lmul_left_apply
added
theorem
algebra.lmul_left_eq_zero_iff
added
theorem
algebra.lmul_left_injective
added
theorem
algebra.lmul_left_mul
added
theorem
algebra.lmul_left_one
added
def
algebra.lmul_left_right
added
theorem
algebra.lmul_left_right_apply
added
theorem
algebra.lmul_left_zero_eq_zero
added
def
algebra.lmul_right
added
theorem
algebra.lmul_right_apply
added
theorem
algebra.lmul_right_eq_zero_iff
added
theorem
algebra.lmul_right_injective
added
theorem
algebra.lmul_right_mul
added
theorem
algebra.lmul_right_one
added
theorem
algebra.lmul_right_zero_eq_zero
added
theorem
algebra.pow_lmul_left
added
theorem
algebra.pow_lmul_right
Modified
src/algebra/algebra/operations.lean
Modified
src/linear_algebra/alternating.lean
Modified
src/linear_algebra/determinant.lean
Renamed
src/linear_algebra/multilinear.lean
to
src/linear_algebra/multilinear/basic.lean
deleted
def
multilinear_map.dom_coprod'
deleted
theorem
multilinear_map.dom_coprod'_apply
deleted
def
multilinear_map.dom_coprod
deleted
theorem
multilinear_map.dom_coprod_dom_dom_congr_sum_congr
Created
src/linear_algebra/multilinear/tensor_product.lean
added
def
multilinear_map.dom_coprod'
added
theorem
multilinear_map.dom_coprod'_apply
added
def
multilinear_map.dom_coprod
added
theorem
multilinear_map.dom_coprod_dom_dom_congr_sum_congr
Modified
src/linear_algebra/pi_tensor_product.lean
Modified
src/ring_theory/nilpotent.lean
Modified
src/topology/algebra/multilinear.lean