Commit 2023-11-27 10:05 4b30f25b

refactor(Data/Matrix/Basic): use a defeq for scalar that matches its docstring (#8115) This changes the defeq from scalar a = a • 1 to scalar a = diagonal fun _ => a, which has the nice bonus of making algebraMap_eq_diagonal true by rfl. As a result, we need a new smul_one_eq_diagonal lemma to rewrite diagonal fun _ => a back into a • 1, along with some variants for convenience. In the long term we could generalize this to non-unital rings, now that it needs no 1.