Commit 2021-09-24 11:04 48883dcd

View on Github →

chore(algebra/basic): split out facts about lmul (#9300)

Estimated changes

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_mul
deleted theorem algebra.lmul_left_one
deleted def algebra.lmul_right
deleted theorem algebra.lmul_right_apply
deleted theorem algebra.lmul_right_mul
deleted theorem algebra.lmul_right_one
deleted theorem algebra.pow_lmul_left
deleted theorem algebra.pow_lmul_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 theorem algebra.lmul_left_mul
added theorem algebra.lmul_left_one
added theorem algebra.lmul_right_mul
added theorem algebra.lmul_right_one
added theorem algebra.pow_lmul_left
added theorem algebra.pow_lmul_right