# Quadratic forms #

This file defines quadratic forms over a R-module M. A quadratic form is a map Q : M → R such that (to_fun_smul) Q (a • x) = a * a * Q x (polar_...) The map polar Q := λ x y, Q (x + y) - Q x - Q y is bilinear. They come with a scalar multiplication, (a • Q) x = Q (a • x) = a * a * Q x, and composition with linear maps f, Q.comp f x = Q (f x).

## Main definitions #

• quadratic_form.associated: associated bilinear form
• quadratic_form.pos_def: positive definite quadratic forms
• quadratic_form.anisotropic: anisotropic quadratic forms
• quadratic_form.discr: discriminant of a quadratic form

## Main statements #

• quadratic_form.associated_left_inverse,
• quadratic_form.associated_right_inverse: in a commutative ring where 2 has an inverse, there is a correspondence between quadratic forms and symmetric bilinear forms
• bilin_form.exists_orthogonal_basis: There exists an orthogonal basis with respect to any nondegenerate, symmetric bilinear form B.

## Notation #

In this file, the variable R is used when a ring structure is sufficient and R₁ is used when specifically a comm_ring is required. This allows us to keep [module R M] and [module R₁ M] assumptions in the variables without confusion between * from ring and * from comm_ring.

The variable S is used when R itself has a • action.

## Tags #

def quadratic_form.polar {R : Type u_2} {M : Type u_3} [ring R] (f : M → R) (x y : M) :
R

Up to a factor 2, Q.polar is the associated bilinear form for a quadratic form Q.d

Source of this name: https://en.wikipedia.org/wiki/Quadratic_form#Generalization

Equations
• y = f (x + y) - f x - f y
theorem quadratic_form.polar_add {R : Type u_2} {M : Type u_3} [ring R] (f g : M → R) (x y : M) :
quadratic_form.polar (f + g) x y = y + y
theorem quadratic_form.polar_neg {R : Type u_2} {M : Type u_3} [ring R] (f : M → R) (x y : M) :
y = - y
theorem quadratic_form.polar_smul {S : Type u_1} {R : Type u_2} {M : Type u_3} [ring R] [monoid S] [ R] (f : M → R) (s : S) (x y : M) :
theorem quadratic_form.polar_comm {R : Type u_2} {M : Type u_3} [ring R] (f : M → R) (x y : M) :
y = x
structure quadratic_form (R : Type u) (M : Type v) [ring R] [ M] :
Type (max u v)
• to_fun : M → R
• to_fun_smul : ∀ (a : R) (x : M), c.to_fun (a x) = (a * a) * c.to_fun x
• polar_add_left' : ∀ (x x' y : M), (x + x') y = + y
• polar_smul_left' : ∀ (a : R) (x y : M), (a x) y = a
• polar_add_right' : ∀ (x y y' : M), (y + y') = + y'
• polar_smul_right' : ∀ (a : R) (x y : M), (a y) = a

A quadratic form over a module.

@[instance]
def quadratic_form.has_coe_to_fun {R : Type u_2} {M : Type u_3} [ring R] [ M] :
Equations
@[simp]
theorem quadratic_form.to_fun_eq_apply {R : Type u_2} {M : Type u_3} [ring R] [ M] {Q : M} :

The simp normal form for a quadratic form is coe_fn, not to_fun.

theorem quadratic_form.map_smul {R : Type u_2} {M : Type u_3} [ring R] [ M] {Q : M} (a : R) (x : M) :
Q (a x) = (a * a) * Q x
theorem quadratic_form.map_add_self {R : Type u_2} {M : Type u_3} [ring R] [ M] {Q : M} (x : M) :
Q (x + x) = 4 * Q x
@[simp]
theorem quadratic_form.map_zero {R : Type u_2} {M : Type u_3} [ring R] [ M] {Q : M} :
Q 0 = 0
@[simp]
theorem quadratic_form.map_neg {R : Type u_2} {M : Type u_3} [ring R] [ M] {Q : M} (x : M) :
Q (-x) = Q x
theorem quadratic_form.map_sub {R : Type u_2} {M : Type u_3} [ring R] [ M] {Q : M} (x y : M) :
Q (x - y) = Q (y - x)
@[simp]
theorem quadratic_form.polar_zero_left {R : Type u_2} {M : Type u_3} [ring R] [ M] {Q : M} (y : M) :
= 0
@[simp]
theorem quadratic_form.polar_add_left {R : Type u_2} {M : Type u_3} [ring R] [ M] {Q : M} (x x' y : M) :
(x + x') y = + y
@[simp]
theorem quadratic_form.polar_smul_left {R : Type u_2} {M : Type u_3} [ring R] [ M] {Q : M} (a : R) (x y : M) :
(a x) y = a *
@[simp]
theorem quadratic_form.polar_neg_left {R : Type u_2} {M : Type u_3} [ring R] [ M] {Q : M} (x y : M) :
y = -
@[simp]
theorem quadratic_form.polar_sub_left {R : Type u_2} {M : Type u_3} [ring R] [ M] {Q : M} (x x' y : M) :
(x - x') y = - y
@[simp]
theorem quadratic_form.polar_zero_right {R : Type u_2} {M : Type u_3} [ring R] [ M] {Q : M} (y : M) :
= 0
@[simp]
theorem quadratic_form.polar_add_right {R : Type u_2} {M : Type u_3} [ring R] [ M] {Q : M} (x y y' : M) :
(y + y') = + y'
@[simp]
theorem quadratic_form.polar_smul_right {R : Type u_2} {M : Type u_3} [ring R] [ M] {Q : M} (a : R) (x y : M) :
(a y) = a *
@[simp]
theorem quadratic_form.polar_neg_right {R : Type u_2} {M : Type u_3} [ring R] [ M] {Q : M} (x y : M) :
(-y) = -
@[simp]
theorem quadratic_form.polar_sub_right {R : Type u_2} {M : Type u_3} [ring R] [ M] {Q : M} (x y y' : M) :
(y - y') = - y'
@[simp]
theorem quadratic_form.polar_self {R : Type u_2} {M : Type u_3} [ring R] [ M] {Q : M} (x : M) :
= 2 * Q x
@[simp]
theorem quadratic_form.polar_smul_left_of_tower {S : Type u_1} {R : Type u_2} {M : Type u_3} [ring R] [ M] {Q : M} [ R] [ M] [ M] (a : S) (x y : M) :
(a x) y = a
@[simp]
theorem quadratic_form.polar_smul_right_of_tower {S : Type u_1} {R : Type u_2} {M : Type u_3} [ring R] [ M] {Q : M} [ R] [ M] [ M] (a : S) (x y : M) :
(a y) = a
@[ext]
theorem quadratic_form.ext {R : Type u_2} {M : Type u_3} [ring R] [ M] {Q Q' : M} (H : ∀ (x : M), Q x = Q' x) :
Q = Q'
@[instance]
def quadratic_form.has_zero {R : Type u_2} {M : Type u_3} [ring R] [ M] :
Equations
@[simp]
theorem quadratic_form.coe_fn_zero {R : Type u_2} {M : Type u_3} [ring R] [ M] :
0 = 0
@[simp]
theorem quadratic_form.zero_apply {R : Type u_2} {M : Type u_3} [ring R] [ M] (x : M) :
0 x = 0
@[instance]
def quadratic_form.inhabited {R : Type u_2} {M : Type u_3} [ring R] [ M] :
Equations
@[instance]
def quadratic_form.has_add {R : Type u_2} {M : Type u_3} [ring R] [ M] :
Equations
@[simp]
theorem quadratic_form.coe_fn_add {R : Type u_2} {M : Type u_3} [ring R] [ M] (Q Q' : M) :
(Q + Q') = Q + Q'
@[simp]
theorem quadratic_form.add_apply {R : Type u_2} {M : Type u_3} [ring R] [ M] (Q Q' : M) (x : M) :
(Q + Q') x = Q x + Q' x
@[instance]
def quadratic_form.has_neg {R : Type u_2} {M : Type u_3} [ring R] [ M] :
Equations
@[simp]
theorem quadratic_form.coe_fn_neg {R : Type u_2} {M : Type u_3} [ring R] [ M] (Q : M) :
@[simp]
theorem quadratic_form.neg_apply {R : Type u_2} {M : Type u_3} [ring R] [ M] (Q : M) (x : M) :
(-Q) x = -Q x
@[instance]
def quadratic_form.add_comm_group {R : Type u_2} {M : Type u_3} [ring R] [ M] :
Equations
@[simp]
theorem quadratic_form.coe_fn_sub {R : Type u_2} {M : Type u_3} [ring R] [ M] (Q Q' : M) :
(Q - Q') = Q - Q'
@[simp]
theorem quadratic_form.sub_apply {R : Type u_2} {M : Type u_3} [ring R] [ M] (Q Q' : M) (x : M) :
(Q - Q') x = Q x - Q' x
def quadratic_form.coe_fn_add_monoid_hom {R : Type u_2} {M : Type u_3} [ring R] [ M] :
→+ M → R

@coe_fn (quadratic_form R M) as an add_monoid_hom.

This API mirrors add_monoid_hom.coe_fn.

Equations
@[simp]
theorem quadratic_form.coe_fn_add_monoid_hom_apply {R : Type u_2} {M : Type u_3} [ring R] [ M] (x : M) (ᾰ : M) :
@[simp]
theorem quadratic_form.eval_add_monoid_hom_apply {R : Type u_2} {M : Type u_3} [ring R] [ M] (m : M) (ᾰ : M) :
def quadratic_form.eval_add_monoid_hom {R : Type u_2} {M : Type u_3} [ring R] [ M] (m : M) :
→+ R

Evaluation on a particular element of the module M is an additive map over quadratic forms.

Equations
@[simp]
theorem quadratic_form.coe_fn_sum {R : Type u_2} {M : Type u_3} [ring R] [ M] {ι : Type u_1} (Q : ι → ) (s : finset ι) :
∑ (i : ι) in s, Q i = ∑ (i : ι) in s, (Q i)
@[simp]
theorem quadratic_form.sum_apply {R : Type u_2} {M : Type u_3} [ring R] [ M] {ι : Type u_1} (Q : ι → ) (s : finset ι) (x : M) :
(∑ (i : ι) in s, Q i) x = ∑ (i : ι) in s, (Q i) x
@[instance]
def quadratic_form.has_scalar {S : Type u_1} {R : Type u_2} {M : Type u_3} [ring R] [ M] [monoid S] [ R] [ R] :
M)

quadratic_form R M inherits the scalar action from any algebra over R.

When R is commutative, this provides an R-action via algebra.id.

Equations
@[simp]
theorem quadratic_form.coe_fn_smul {S : Type u_1} {R : Type u_2} {M : Type u_3} [ring R] [ M] [monoid S] [ R] [ R] (a : S) (Q : M) :
(a Q) = a Q
@[simp]
theorem quadratic_form.smul_apply {S : Type u_1} {R : Type u_2} {M : Type u_3} [ring R] [ M] [monoid S] [ R] [ R] (a : S) (Q : M) (x : M) :
(a Q) x = a Q x
@[instance]
def quadratic_form.distrib_mul_action {S : Type u_1} {R : Type u_2} {M : Type u_3} [ring R] [ M] [monoid S] [ R] [ R] :
M)
Equations
@[instance]
def quadratic_form.module {S : Type u_1} {R : Type u_2} {M : Type u_3} [ring R] [ M] [semiring S] [ R] [ R] :
M)
Equations
def quadratic_form.comp {R : Type u_2} {M : Type u_3} [ring R] [ M] {N : Type v} [ N] (Q : N) (f : M →ₗ[R] N) :

Compose the quadratic form with a linear function.

Equations
@[simp]
theorem quadratic_form.comp_apply {R : Type u_2} {M : Type u_3} [ring R] [ M] {N : Type v} [ N] (Q : N) (f : M →ₗ[R] N) (x : M) :
(Q.comp f) x = Q (f x)
def quadratic_form.mk_left {M : Type u_3} {R₁ : Type u_4} [comm_ring R₁] [module R₁ M] (f : M → R₁) (to_fun_smul : ∀ (a : R₁) (x : M), f (a x) = (a * a) * f x) (polar_add_left : ∀ (x x' y : M), (x + x') y = y + y) (polar_smul_left : ∀ (a : R₁) (x y : M), (a x) y = a * y) :
M

Create a quadratic form in a commutative ring by proving only one side of the bilinearity.

Equations
def quadratic_form.lin_mul_lin {M : Type u_3} {R₁ : Type u_4} [comm_ring R₁] [module R₁ M] (f g : M →ₗ[R₁] R₁) :
M

The product of linear forms is a quadratic form.

Equations
@[simp]
theorem quadratic_form.lin_mul_lin_apply {M : Type u_3} {R₁ : Type u_4} [comm_ring R₁] [module R₁ M] (f g : M →ₗ[R₁] R₁) (x : M) :
x = (f x) * g x
@[simp]
theorem quadratic_form.add_lin_mul_lin {M : Type u_3} {R₁ : Type u_4} [comm_ring R₁] [module R₁ M] (f g h : M →ₗ[R₁] R₁) :
@[simp]
theorem quadratic_form.lin_mul_lin_add {M : Type u_3} {R₁ : Type u_4} [comm_ring R₁] [module R₁ M] (f g h : M →ₗ[R₁] R₁) :
@[simp]
theorem quadratic_form.lin_mul_lin_comp {M : Type u_3} {R₁ : Type u_4} [comm_ring R₁] [module R₁ M] {N : Type v} [module R₁ N] (f g : M →ₗ[R₁] R₁) (h : N →ₗ[R₁] M) :
h = (g.comp h)
def quadratic_form.proj {R₁ : Type u_4} [comm_ring R₁] {n : Type u_5} (i j : n) :
(n → R₁)

proj i j is the quadratic form mapping the vector x : n → R₁ to x i * x j

Equations
@[simp]
theorem quadratic_form.proj_apply {R₁ : Type u_4} [comm_ring R₁] {n : Type u_5} (i j : n) (x : n → R₁) :
j) x = (x i) * x j

### Associated bilinear forms #

Over a commutative ring with an inverse of 2, the theory of quadratic forms is basically identical to that of symmetric bilinear forms. The map from quadratic forms to bilinear forms giving this identification is called the associated quadratic form.

theorem bilin_form.polar_to_quadratic_form {R : Type u_2} {M : Type u_3} [ring R] [ M] {B : M} (x y : M) :
quadratic_form.polar (λ (x : M), B x x) x y = B x y + B y x
def bilin_form.to_quadratic_form {R : Type u_2} {M : Type u_3} [ring R] [ M] (B : M) :

A bilinear form gives a quadratic form by applying the argument twice.

Equations
@[simp]
theorem bilin_form.to_quadratic_form_apply {R : Type u_2} {M : Type u_3} [ring R] [ M] (B : M) (x : M) :
def quadratic_form.associated_hom (S : Type u_1) {R : Type u_2} {M : Type u_3} [ring R] [ M] [ R] [invertible 2] :

associated_hom is the map that sends a quadratic form on a module M over R to its associated symmetric bilinear form. As provided here, this has the structure of an S-linear map where S is a commutative subring of R.

Over a commutative ring, use associated, which gives an R-linear map. Over a general ring with no nontrivial distinguished commutative subring, use associated', which gives an additive homomorphism (or more precisely a ℤ-linear map.)

Equations
@[simp]
theorem quadratic_form.associated_apply {S : Type u_1} {R : Type u_2} {M : Type u_3} [ring R] [ M] [ R] [invertible 2] {Q : M} (x y : M) :
x y = ( 2) * (Q (x + y) - Q x - Q y)
theorem quadratic_form.associated_is_sym {S : Type u_1} {R : Type u_2} {M : Type u_3} [ring R] [ M] [ R] [invertible 2] {Q : M} :
@[simp]
theorem quadratic_form.associated_comp {S : Type u_1} {R : Type u_2} {M : Type u_3} [ring R] [ M] [ R] [invertible 2] {Q : M} {N : Type v} [ N] (f : N →ₗ[R] M) :
(Q.comp f) = .comp f f
theorem quadratic_form.associated_to_quadratic_form {S : Type u_1} {R : Type u_2} {M : Type u_3} [ring R] [ M] [ R] [invertible 2] (B : M) (x y : M) :
y = ( 2) * (B x y + B y x)
theorem quadratic_form.associated_left_inverse {S : Type u_1} {R : Type u_2} {M : Type u_3} [ring R] [ M] [ R] [invertible 2] {B₁ : M} (h : sym_bilin_form.is_sym B₁) :
theorem quadratic_form.associated_right_inverse {S : Type u_1} {R : Type u_2} {M : Type u_3} [ring R] [ M] [ R] [invertible 2] {Q : M} :
theorem quadratic_form.associated_eq_self_apply {S : Type u_1} {R : Type u_2} {M : Type u_3} [ring R] [ M] [ R] [invertible 2] {Q : M} (x : M) :
x x = Q x
def quadratic_form.associated' {R : Type u_2} {M : Type u_3} [ring R] [ M] [invertible 2] :

associated' is the ℤ-linear map that sends a quadratic form on a module M over R to its associated symmetric bilinear form.

theorem quadratic_form.exists_quadratic_form_neq_zero {R : Type u_2} {M : Type u_3} [ring R] [ M] [invertible 2] [nontrivial M] {Q : M} (hB₁ : .nondegenerate) :
∃ (x : M), Q x 0

There exists a non-null vector with respect to any quadratic form Q whose associated bilinear form is non-degenerate, i.e. there exists x such that Q x ≠ 0.

def quadratic_form.associated {M : Type u_3} {R₁ : Type u_4} [comm_ring R₁] [module R₁ M] [invertible 2] :
M →ₗ[R₁] M

associated is the linear map that sends a quadratic form over a commutative ring to its associated symmetric bilinear form.

@[simp]
theorem quadratic_form.associated_lin_mul_lin {M : Type u_3} {R₁ : Type u_4} [comm_ring R₁] [module R₁ M] [invertible 2] (f g : M →ₗ[R₁] R₁) :
def quadratic_form.anisotropic {R : Type u_2} {M : Type u_3} [ring R] [ M] (Q : M) :
Prop

An anisotropic quadratic form is zero only on zero vectors.

Equations
theorem quadratic_form.not_anisotropic_iff_exists {R : Type u_2} {M : Type u_3} [ring R] [ M] (Q : M) :
¬Q.anisotropic ∃ (x : M) (H : x 0), Q x = 0
theorem quadratic_form.nondegenerate_of_anisotropic {R : Type u_2} {M : Type u_3} [ring R] [ M] [invertible 2] (Q : M) (hB : Q.anisotropic) :

The associated bilinear form of an anisotropic quadratic form is nondegenerate.

def quadratic_form.pos_def {M : Type u_3} {R₂ : Type u} [ordered_ring R₂] [module R₂ M] (Q₂ : M) :
Prop

A positive definite quadratic form is positive on nonzero vectors.

Equations
theorem quadratic_form.pos_def.smul {M : Type u_3} {R : Type u_1} [ M] {Q : M} (h : Q.pos_def) {a : R} (a_pos : 0 < a) :
(a Q).pos_def
theorem quadratic_form.pos_def.add {M : Type u_3} {R₂ : Type u} [ordered_ring R₂] [module R₂ M] (Q Q' : M) (hQ : Q.pos_def) (hQ' : Q'.pos_def) :
(Q + Q').pos_def
theorem quadratic_form.lin_mul_lin_self_pos_def {M : Type u_3} {R : Type u_1} [ M] (f : M →ₗ[R] R) (hf : f.ker = ) :

### Quadratic forms and matrices #

Connect quadratic forms and matrices, in order to explicitly compute with them. The convention is twos out, so there might be a factor 2⁻¹ in the entries of the matrix. The determinant of the matrix is the discriminant of the quadratic form.

def matrix.to_quadratic_form' {R₁ : Type u_4} [comm_ring R₁] {n : Type w} [fintype n] [decidable_eq n] (M : n R₁) :
(n → R₁)

M.to_quadratic_form is the map λ x, col x ⬝ M ⬝ row x as a quadratic form.

Equations
def quadratic_form.to_matrix' {R₁ : Type u_4} [comm_ring R₁] {n : Type w} [fintype n] [decidable_eq n] [invertible 2] (Q : (n → R₁)) :
n R₁

A matrix representation of the quadratic form.

Equations
theorem quadratic_form.to_matrix'_smul {R₁ : Type u_4} [comm_ring R₁] {n : Type w} [fintype n] [decidable_eq n] [invertible 2] (a : R₁) (Q : (n → R₁)) :
@[simp]
theorem quadratic_form.to_matrix'_comp {R₁ : Type u_4} [comm_ring R₁] {n : Type w} [fintype n] [decidable_eq n] [invertible 2] {m : Type w} [decidable_eq m] [fintype m] (Q : (m → R₁)) (f : (n → R₁) →ₗ[R₁] m → R₁) :
def quadratic_form.discr {R₁ : Type u_4} [comm_ring R₁] {n : Type w} [fintype n] [decidable_eq n] [invertible 2] (Q : (n → R₁)) :
R₁

The discriminant of a quadratic form generalizes the discriminant of a quadratic polynomial.

Equations
theorem quadratic_form.discr_smul {R₁ : Type u_4} [comm_ring R₁] {n : Type w} [fintype n] [decidable_eq n] [invertible 2] {Q : (n → R₁)} (a : R₁) :
(a Q).discr = (a ^ * Q.discr
theorem quadratic_form.discr_comp {R₁ : Type u_4} [comm_ring R₁] {n : Type w} [fintype n] [decidable_eq n] [invertible 2] {Q : (n → R₁)} (f : (n → R₁) →ₗ[R₁] n → R₁) :
(Q.comp f).discr = .det) * * Q.discr
@[nolint]
structure quadratic_form.isometry {R : Type u_2} [ring R] {M₁ : Type u_5} {M₂ : Type u_6} [add_comm_group M₁] [add_comm_group M₂] [ M₁] [ M₂] (Q₁ : M₁) (Q₂ : M₂) :
Type (max u_5 u_6)

An isometry between two quadratic spaces M₁, Q₁ and M₂, Q₂ over a ring R, is a linear equivalence between M₁ and M₂ that commutes with the quadratic forms.

def quadratic_form.equivalent {R : Type u_2} [ring R] {M₁ : Type u_5} {M₂ : Type u_6} [add_comm_group M₁] [add_comm_group M₂] [ M₁] [ M₂] (Q₁ : M₁) (Q₂ : M₂) :
Prop

Two quadratic forms over a ring R are equivalent if there exists an isometry between them: a linear equivalence that transforms one quadratic form into the other.

Equations
@[instance]
def quadratic_form.isometry.linear_equiv.has_coe {R : Type u_2} [ring R] {M₁ : Type u_5} {M₂ : Type u_6} [add_comm_group M₁] [add_comm_group M₂] [ M₁] [ M₂] {Q₁ : M₁} {Q₂ : M₂} :
has_coe (Q₁.isometry Q₂) (M₁ ≃ₗ[R] M₂)
Equations
@[instance]
def quadratic_form.isometry.has_coe_to_fun {R : Type u_2} [ring R] {M₁ : Type u_5} {M₂ : Type u_6} [add_comm_group M₁] [add_comm_group M₂] [ M₁] [ M₂] {Q₁ : M₁} {Q₂ : M₂} :
Equations
@[simp]
theorem quadratic_form.isometry.map_app {R : Type u_2} [ring R] {M₁ : Type u_5} {M₂ : Type u_6} [add_comm_group M₁] [add_comm_group M₂] [ M₁] [ M₂] {Q₁ : M₁} {Q₂ : M₂} (f : Q₁.isometry Q₂) (m : M₁) :
Q₂ (f m) = Q₁ m
def quadratic_form.isometry.refl {R : Type u_2} {M : Type u_3} [ring R] [ M] (Q : M) :

The identity isometry from a quadratic form to itself.

Equations
def quadratic_form.isometry.symm {R : Type u_2} [ring R] {M₁ : Type u_5} {M₂ : Type u_6} [add_comm_group M₁] [add_comm_group M₂] [ M₁] [ M₂] {Q₁ : M₁} {Q₂ : M₂} (f : Q₁.isometry Q₂) :
Q₂.isometry Q₁

The inverse isometry of an isometry between two quadratic forms.

Equations
def quadratic_form.isometry.trans {R : Type u_2} [ring R] {M₁ : Type u_5} {M₂ : Type u_6} {M₃ : Type u_7} [add_comm_group M₁] [add_comm_group M₂] [add_comm_group M₃] [ M₁] [ M₂] [ M₃] {Q₁ : M₁} {Q₂ : M₂} {Q₃ : M₃} (f : Q₁.isometry Q₂) (g : Q₂.isometry Q₃) :
Q₁.isometry Q₃

The composition of two isometries between quadratic forms.

Equations
theorem quadratic_form.equivalent.refl {R : Type u_2} {M : Type u_3} [ring R] [ M] (Q : M) :
theorem quadratic_form.equivalent.symm {R : Type u_2} [ring R] {M₁ : Type u_5} {M₂ : Type u_6} [add_comm_group M₁] [add_comm_group M₂] [ M₁] [ M₂] {Q₁ : M₁} {Q₂ : M₂} (h : Q₁.equivalent Q₂) :
Q₂.equivalent Q₁
theorem quadratic_form.equivalent.trans {R : Type u_2} [ring R] {M₁ : Type u_5} {M₂ : Type u_6} {M₃ : Type u_7} [add_comm_group M₁] [add_comm_group M₂] [add_comm_group M₃] [ M₁] [ M₂] [ M₃] {Q₁ : M₁} {Q₂ : M₂} {Q₃ : M₃} (h : Q₁.equivalent Q₂) (h' : Q₂.equivalent Q₃) :
Q₁.equivalent Q₃
theorem bilin_form.nondegenerate_of_anisotropic {R : Type u_2} {M : Type u_3} [ring R] [ M] {B : M} (hB : B.to_quadratic_form.anisotropic) :

A bilinear form is nondegenerate if the quadratic form it is associated with is anisotropic.

theorem bilin_form.exists_bilin_form_self_neq_zero {R : Type u_2} {M : Type u_3} [ring R] [ M] [htwo : invertible 2] [nontrivial M] {B : M} (hB₁ : B.nondegenerate) (hB₂ : sym_bilin_form.is_sym B) :
∃ (x : M), ¬B.is_ortho x x

There exists a non-null vector with respect to any symmetric, nondegenerate bilinear form B on a nontrivial module M over a ring R with invertible 2, i.e. there exists some x : M such that B x x ≠ 0.

theorem bilin_form.exists_orthogonal_basis' {V : Type u} {K : Type v} [field K] [ V] [ V] [hK : invertible 2] {B : V} (hB₁ : B.nondegenerate) (hB₂ : sym_bilin_form.is_sym B) :
∃ (v : basis (fin K V), B.is_Ortho v ∀ (i : , B (v i) (v i) 0
theorem bilin_form.exists_orthogonal_basis {V : Type u} {K : Type v} [field K] [ V] [ V] [hK : invertible 2] {B : V} (hB₁ : B.nondegenerate) (hB₂ : sym_bilin_form.is_sym B) :
∃ (v : basis (fin K V), B.is_Ortho v

Given a nondegenerate symmetric bilinear form B on some vector space V over the field K with invertible 2, there exists an orthogonal basis with respect to B.

def quadratic_form.isometry_of_comp_linear_equiv {R : Type u_2} {M : Type u_3} [ring R] [ M] {M₁ : Type u_5} [add_comm_group M₁] [ M₁] (Q : M) (f : M₁ ≃ₗ[R] M) :

A quadratic form composed with a linear_equiv is isometric to itself.

Equations
def quadratic_form.basis_repr {R : Type u_2} {M : Type u_3} [ring R] [ M] {ι : Type u_6} [fintype ι] (Q : M) (v : R M) :
(ι → R)

Given a quadratic form Q and a basis, basis_repr is the basis representation of Q.

Equations
@[simp]
theorem quadratic_form.basis_repr_apply {R : Type u_2} {M : Type u_3} [ring R] [ M] {ι : Type u_6} [fintype ι] {v : R M} (Q : M) (w : ι → R) :
(Q.basis_repr v) w = Q (∑ (i : ι), w i v i)
def quadratic_form.isometry_basis_repr {R : Type u_2} {M : Type u_3} [ring R] [ M] {ι : Type u_6} [fintype ι] (Q : M) (v : R M) :

A quadratic form is isometric to its bases representations.

Equations
theorem quadratic_form.isometry_of_is_Ortho_apply {M : Type u_3} {R₁ : Type u_4} [comm_ring R₁] [module R₁ M] {ι : Type u_6} [fintype ι] [invertible 2] (Q : M) (v : R₁ M) (hv₂ : v) (w : ι → R₁) :
(Q.basis_repr v) w = ∑ (i : ι), (v i) (v i)) * (w i) * w i
def quadratic_form.weighted_sum_squares {S : Type u_1} (R₁ : Type u_4) [comm_ring R₁] {ι : Type u_6} [fintype ι] [monoid S] [ R₁] [ R₁ R₁] (w : ι → S) :
(ι → R₁)

The weighted sum of squares with respect to some weight as a quadratic form.

The weights are applied using •; typically this definition is used either with S = R₁ or [algebra S R₁], although this is stated more generally.

Equations
• = ∑ (i : ι), w i
@[simp]
theorem quadratic_form.weighted_sum_squares_apply {S : Type u_1} {R₁ : Type u_4} [comm_ring R₁] {ι : Type u_6} [fintype ι] [monoid S] [ R₁] [ R₁ R₁] (w : ι → S) (v : ι → R₁) :
= ∑ (i : ι), w i (v i) * v i
theorem quadratic_form.equivalent_weighted_sum_squares_of_nondegenerate' {V : Type u_7} {K : Type u_8} [field K] [invertible 2] [ V] [ V] (Q : V) (hQ : .nondegenerate) :
∃ (w : units K),
def quadratic_form.isometry_sum_squares {ι : Type u_6} [fintype ι] [decidable_eq ι] (w : ι → ) :

The isometry between a weighted sum of squares on the complex numbers and the sum of squares, i.e. weighted_sum_squares with weight λ i : ι, 1.

Equations
theorem quadratic_form.equivalent_sum_squares {M : Type u_1} [ M] (Q : M) (hQ : .nondegenerate) :

A nondegenerate quadratic form on the complex numbers is equivalent to the sum of squares, i.e. weighted_sum_squares with weight λ i : ι, 1.

def quadratic_form.isometry_sign_weighted_sum_squares {ι : Type u_6} [fintype ι] [decidable_eq ι] (u : ι → ) :

The isometry between a weighted sum of squares with weights u on the (non-zero) real numbers and the weighted sum of squares with weights sign ∘ u.

Equations
theorem quadratic_form.equivalent_one_neg_one_weighted_sum_squared {M : Type u_1} [ M] (Q : M) (hQ : .nondegenerate) :
∃ (w : ), (∀ (i : , w i = -1 w i = 1)

Sylvester's law of inertia: A nondegenerate real quadratic form is equivalent to a weighted sum of squares with the weights being ±1.