instNatCastOfZero — Mathlib

English

If α has 0 and a NatCast, then for every natural m, the natural cast of m as a matrix is the diagonal matrix with m on every diagonal entry.

Русский

Если в α есть 0 и имеется отображение NatCast, то для каждого натурального числа m матрица, получаемая приводением m, равна диагональной матрице, на диагонали которой стоит m.

LaTeX

$$$\operatorname{natCast}(m) = \operatorname{diagonal}(\lambda \_ . m)$$$

Lean4

instance [Zero α] [NatCast α] : NatCast (Matrix n n α) where natCast m := diagonal fun _ => m

Похожие утверждения