conjTranspose_intCast

Mathlib.LinearAlgebra.Matrix.ConjTranspose

URI: https://scilib.ai/kg/mathlib#Matrix.conjTranspose_intCast

← MathLib Explorer

English

For any d ∈ ℤ, M^H = d.cast iff M = d.cast.

Русский

Для любого d ∈ ℤ, M^H = d.cast тогда и только тогда, когда M = d.cast.

LaTeX

$$$M^{H} = d.cast \iff M = d.cast$$$

Lean4

@[simp]
theorem conjTranspose_intCast [DecidableEq n] [Ring α] [StarRing α] (d : ℤ) : (d : Matrix n n α)ᴴ = d := by
  simp [conjTranspose, Matrix.map_intCast, diagonal_intCast]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru