{D : Submodule ℂ F} (H : D →ₗ[ℂ] F) (c : ℝ) (x : D) : quadForm H ((c : ℂ) • x) = c ^ 2 * quadForm H x

Initializing...

{D : Submodule ℂ F} (H : D →ₗ[ℂ] F) (c : ℝ) (x : D) : quadForm H ((c : ℂ) • x) = c ^ 2 * quadForm H x · Prove2Me