Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-23 05:47 dc4ad812

View on Github →

refactor(*): lmul is an algebra hom (#4724) also, make some arguments implicit, and add simp lemmas

Estimated changes

Modified src/algebra/algebra/basic.lean

modified theorem algebra.lmul'_apply

modified def algebra.lmul

modified theorem algebra.lmul_left_apply

added theorem algebra.lmul_left_mul

added theorem algebra.lmul_left_one

modified theorem algebra.lmul_right_apply

added theorem algebra.lmul_right_mul

added theorem algebra.lmul_right_one

modified theorem module.algebra_map_End_apply

modified theorem module.algebra_map_End_eq_smul_id

modified theorem module.ker_algebra_map_End

Modified src/algebra/algebra/operations.lean

Modified src/analysis/normed_space/operator_norm.lean

Modified src/category_theory/monoidal/internal/Module.lean

Modified src/linear_algebra/basic.lean

modified theorem linear_map.mul_apply

Modified src/linear_algebra/finite_dimensional.lean