Theorems · Theorem · linear algebra

Matrix.conjTranspose_smul

∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [inst : Star R] [inst_1 : Star α] [inst_2 : SMul R α]
  [StarModule R α] (c : R) (M : Matrix m n α), (c • M).conjTranspose = star c • M.conjTranspose

Note that StarModule is quite a strong requirement; as such we also provide the following variants which this lemma would not apply to: * Matrix.conjTranspose_smul_non_comm * Matrix.conjTranspose_nsmul * Matrix.conjTranspose_zsmul * Matrix.conjTranspose_natCast_smul * Matrix.conjTranspose_intCast_smul * Matrix.conjTranspose_inv_natCast_smul * Matrix.conjTranspose_inv_intCast_smul * Matrix.conjTranspose_ratCast_smul

Defined in

Mathlib.LinearAlgebra.Matrix.ConjTranspose

Cited by

5 results in Mathlib

Foundations

Depth 16 from the axioms · uses propext, Quot.sound

Assumes

StarStarSMulStarModule