Theorems · Definition · number theory

QuadraticForm.toMatrix

{R : Type u_3} →
  {N : Type u_5} →
    {n : Type w} →
      [Fintype n] →
        [DecidableEq n] →
          [inst : CommRing R] →
            [Invertible 2] →
              [inst_2 : AddCommGroup N] → [inst_3 : Module R N] → Module.Basis n R N → QuadraticForm R N → Matrix n n R

A matrix representation of the quadratic form Q : QuadraticForm R N with respect to a given basis. See also QuadraticForm.toMatrix' for the special case of N = n → R with the standard basis.

Defined in

Mathlib.LinearAlgebra.QuadraticForm.Basic

Cited by

8 results in Mathlib

Foundations

Depth 89 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeDecidableEqCommRingInvertibleAddCommGroupModule