generalLinearGroup_smul_def — Mathlib

English

A form of the previous statement expressing the same action equality in a different notation.

Русский

Форма предыдущего утверждения, выраженная другой нотацией той же самой операцией действия.

LaTeX

$$$ g \cdot x = x.map g.toLinearEquiv.toLinearMap(g.toLinearEquiv.injective) $$$

Lean4

theorem generalLinearGroup_smul_def (g : LinearMap.GeneralLinearGroup K V) (x : ℙ K V) :
    g • x = x.map g.toLinearEquiv.toLinearMap g.toLinearEquiv.injective := by rfl

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