conjTranspose_inv_ofNat_smul — Mathlib

English

Let c ∈ ℕ with [c.AtLeastTwo]. The inverse-scalar version holds for the nat-cast: ((OfNat.ofNat c : R)⁻¹ • M)^H = (OfNat.ofNat c : R)⁻¹ • M^H.

Русский

Пусть c ∈ ℕ с условием c ≥ 2. Обратный скаляр через приведение натурального числа: ((OfNat.ofNat c : R)⁻¹ • M)^H = (OfNat.ofNat c : R)⁻¹ • M^H.

LaTeX

$$$ ((\operatorname{OfNat.ofNat} c : R)^{-1} \cdot M)^H = (\operatorname{OfNat.ofNat} c : R)^{-1} \cdot M^H $$$

Lean4

@[simp]
theorem conjTranspose_inv_ofNat_smul [DivisionSemiring R] [AddCommMonoid α] [StarAddMonoid α] [Module R α] (c : ℕ)
    [c.AtLeastTwo] (M : Matrix m n α) : ((ofNat(c) : R)⁻¹ • M)ᴴ = (OfNat.ofNat c : R)⁻¹ • Mᴴ :=
  conjTranspose_inv_natCast_smul c M

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