instMulActionSpecialLinearGroupFixedDetMatrix

English

The scalar action on the underlying matrix coe is consistent: (g • A).val = g · A.1 with A ∈ FixedDetMatrix(m).

Русский

Согласованность действия скаляра на базовой матрице: (g • A).val = g · A.1.

LaTeX

$$$ (g \cdot A).1 = g \cdot A.1 $ for $g \in SL(n,R)$ and $A \in FixedDetMatrix(m)$.$$

Lean4

instance (m : R) : MulAction (SpecialLinearGroup n R) (FixedDetMatrix n R m)
    where
  one_smul b := by rw [smul_def]; simp only [coe_one, one_mul, Subtype.coe_eta]
  mul_smul x y b := by simp_rw [smul_def, ← mul_assoc, coe_mul]

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