smul_def — Mathlib

English

The action of SL(n,R) on FixedDetMatrix(m) satisfies the standard axioms: 1•A = A and (xy)•A = x•(y•A).

Русский

Действие SL(n,R) на FixedDetMatrix(m) удовлетворяет обычным аксиомам: 1·A = A и (xy)·A = x·(y·A).

LaTeX

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

Lean4

theorem smul_def (m : R) (g : SpecialLinearGroup n R) (A : (FixedDetMatrix n R m)) :
    g • A = ⟨g * A.1, by simp only [det_mul, SpecialLinearGroup.det_coe, A.2, one_mul]⟩ :=
  rfl

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