groupSMul — Mathlib

English

If a bilinear form B is symmetric, then its image under any group action a•B is symmetric.

Русский

Если билинейная форма B симметрична, то ее образ под действием группы a•B симметричен.

LaTeX

$$$B.IsRefl \Rightarrow (a \cdot B).IsRefl$$$

Lean4

protected theorem groupSMul {α} [Group α] [DistribMulAction α R] [SMulCommClass R α R] (a : α) {B : BilinForm R M}
    (hB : B.IsRefl) : (a • B).IsRefl := fun x y => (smul_eq_zero_iff_eq _).mpr ∘ hB x y ∘ (smul_eq_zero_iff_eq _).mp

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