English
Let ι be an index type and α a type with a star operation. For any v: m → α, the conjugate transpose of the matrix obtained by repeating the row v equals the matrix obtained by repeating the star of v as columns: (replicateRow ι v)ᴴ = replicateCol ι (star v).
Русский
Пусть ι — индексный тип и α — множество с операцией сопряжения. Для любого v : m → α верно, что конъюгированное транспонирование матрицы, полученной повторением строки v, равно матрице, полученной повторением звёздочки v по столбцам: (replicateRow ι v)ᴴ = replicateCol ι (star v).
LaTeX
$$$ (\mathrm{replicateRow}\ \iota\ v)^H = \mathrm{replicateCol}\ \iota\ (\star v) $$$
Lean4
@[simp]
theorem conjTranspose_replicateRow [Star α] (v : m → α) : (replicateRow ι v)ᴴ = replicateCol ι (star v) :=
by
ext
rfl
