English
Let R be a semiring and α an additive commutative monoid with a star, and assume a scalar c coming from a nat-to-R cast via OfNat. The conjugate transpose commutes with this scalar: ((OfNat.ofNat c : R) • M)^H = (OfNat.ofNat c : R) • M^H.
Русский
Пусть R — полугруппа, α — аддитивный коммутативный моноид с операцией звезда, и коэффициент c дан через приведение натурального числа к R. Сопряжённое транспонирование commuting с этим скаляром: ((OfNat.ofNat c : R) • M)^H = (OfNat.ofNat c : R) • M^H.
LaTeX
$$$ ((\operatorname{OfNat.ofNat} c : R) \cdot M)^H = (\operatorname{OfNat.ofNat} c : R) \cdot M^H $$$
Lean4
@[simp]
theorem conjTranspose_ofNat_smul [Semiring R] [AddCommMonoid α] [StarAddMonoid α] [Module R α] (c : ℕ) [c.AtLeastTwo]
(M : Matrix m n α) : ((ofNat(c) : R) • M)ᴴ = (OfNat.ofNat c : R) • Mᴴ :=
conjTranspose_natCast_smul c M
