mathlib documentation

linear_algebra.bilinear_form

Bilinear form

This file defines a bilinear form over a module. Basic ideas such as orthogonality are also introduced, as well as reflexivive, symmetric and alternating bilinear forms. Adjoints of linear maps with respect to a bilinear form are also introduced.

A bilinear form on an R-module M, is a function from M x M to R, that is linear in both arguments

Notations

Given any term B of type bilin_form, due to a coercion, can use the notation B x y to refer to the function field, ie. B x y = B.bilin x y.

References

Tags

Bilinear form,

structure bilin_form (R : Type u) (M : Type v) [ring R] [add_comm_group M] [module R M] :
Type (max u v)
  • bilin : M → M → R
  • bilin_add_left : ∀ (x y z : M), c.bilin (x + y) z = c.bilin x z + c.bilin y z
  • bilin_smul_left : ∀ (a : R) (x y : M), c.bilin (a x) y = a * c.bilin x y
  • bilin_add_right : ∀ (x y z : M), c.bilin x (y + z) = c.bilin x y + c.bilin x z
  • bilin_smul_right : ∀ (a : R) (x y : M), c.bilin x (a y) = a * c.bilin x y

A bilinear form over a module

def linear_map.to_bilin {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] :
(M →ₗ[R] M →ₗ[R] R)bilin_form R M

A map with two arguments that is linear in both is a bilinear form

Equations
@[instance]
def bilin_form.has_coe_to_fun {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] :

Equations
@[simp]
theorem bilin_form.coe_fn_mk {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] (f : M → M → R) (h₁ : ∀ (x y z : M), f (x + y) z = f x z + f y z) (h₂ : ∀ (a : R) (x y : M), f (a x) y = a * f x y) (h₃ : ∀ (x y z : M), f x (y + z) = f x y + f x z) (h₄ : ∀ (a : R) (x y : M), f x (a y) = a * f x y) :
{bilin := f, bilin_add_left := h₁, bilin_smul_left := h₂, bilin_add_right := h₃, bilin_smul_right := h₄} = f

theorem bilin_form.coe_fn_congr {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {B : bilin_form R M} {x x' y y' : M} :
x = x'y = y'B x y = B x' y'

theorem bilin_form.add_left {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {B : bilin_form R M} (x y z : M) :
B (x + y) z = B x z + B y z

theorem bilin_form.smul_left {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {B : bilin_form R M} (a : R) (x y : M) :
B (a x) y = a * B x y

theorem bilin_form.add_right {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {B : bilin_form R M} (x y z : M) :
B x (y + z) = B x y + B x z

theorem bilin_form.smul_right {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {B : bilin_form R M} (a : R) (x y : M) :
B x (a y) = a * B x y

theorem bilin_form.zero_left {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {B : bilin_form R M} (x : M) :
B 0 x = 0

theorem bilin_form.zero_right {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {B : bilin_form R M} (x : M) :
B x 0 = 0

theorem bilin_form.neg_left {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {B : bilin_form R M} (x y : M) :
B (-x) y = -B x y

theorem bilin_form.neg_right {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {B : bilin_form R M} (x y : M) :
B x (-y) = -B x y

theorem bilin_form.sub_left {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {B : bilin_form R M} (x y z : M) :
B (x - y) z = B x z - B y z

theorem bilin_form.sub_right {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {B : bilin_form R M} (x y z : M) :
B x (y - z) = B x y - B x z

@[ext]
theorem bilin_form.ext {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {B D : bilin_form R M} :
(∀ (x y : M), B x y = D x y)B = D

@[instance]
def bilin_form.add_comm_group {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] :

Equations
theorem bilin_form.add_apply {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {B D : bilin_form R M} (x y : M) :
(B + D) x y = B x y + D x y

theorem bilin_form.neg_apply {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {B : bilin_form R M} (x y : M) :
(-B) x y = -B x y

@[instance]
def bilin_form.inhabited {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] :

Equations
@[instance]
def bilin_form.to_module {M : Type v} [add_comm_group M] {R₂ : Type u_1} [comm_ring R₂] [module R₂ M] :
module R₂ (bilin_form R₂ M)

Equations
theorem bilin_form.smul_apply {M : Type v} [add_comm_group M] {R₂ : Type u_1} [comm_ring R₂] [module R₂ M] (F : bilin_form R₂ M) (a : R₂) (x y : M) :
(a F) x y = a F x y

def bilin_form.to_linear_map {M : Type v} [add_comm_group M] {R₂ : Type u_1} [comm_ring R₂] [module R₂ M] :
bilin_form R₂ M(M →ₗ[R₂] M →ₗ[R₂] R₂)

B.to_linear_map applies B on the left argument, then the right.

Equations
def bilin_form.bilin_linear_map_equiv {M : Type v} [add_comm_group M] {R₂ : Type u_1} [comm_ring R₂] [module R₂ M] :
bilin_form R₂ M ≃ₗ[R₂] M →ₗ[R₂] M →ₗ[R₂] R₂

Bilinear forms are equivalent to maps with two arguments that is linear in both.

Equations
theorem bilin_form.coe_fn_to_linear_map {M : Type v} [add_comm_group M] {R₂ : Type u_1} [comm_ring R₂] [module R₂ M] (F : bilin_form R₂ M) (x : M) :

theorem bilin_form.map_sum_left {M : Type v} [add_comm_group M] {R₂ : Type u_1} [comm_ring R₂] [module R₂ M] {α : Type u_2} (B : bilin_form R₂ M) (t : finset α) (g : α → M) (w : M) :
B (∑ (i : α) in t, g i) w = ∑ (i : α) in t, B (g i) w

theorem bilin_form.map_sum_right {M : Type v} [add_comm_group M] {R₂ : Type u_1} [comm_ring R₂] [module R₂ M] {α : Type u_2} (B : bilin_form R₂ M) (t : finset α) (g : α → M) (v : M) :
B v (∑ (i : α) in t, g i) = ∑ (i : α) in t, B v (g i)

def bilin_form.comp {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {N : Type w} [add_comm_group N] [module R N] :
bilin_form R N(M →ₗ[R] N)(M →ₗ[R] N)bilin_form R M

Apply a linear map on the left and right argument of a bilinear form.

Equations
def bilin_form.comp_left {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] :
bilin_form R M(M →ₗ[R] M)bilin_form R M

Apply a linear map to the left argument of a bilinear form.

Equations
def bilin_form.comp_right {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] :
bilin_form R M(M →ₗ[R] M)bilin_form R M

Apply a linear map to the right argument of a bilinear form.

Equations
@[simp]
theorem bilin_form.comp_left_comp_right {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] (B : bilin_form R M) (l r : M →ₗ[R] M) :
(B.comp_left l).comp_right r = B.comp l r

@[simp]
theorem bilin_form.comp_right_comp_left {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] (B : bilin_form R M) (l r : M →ₗ[R] M) :
(B.comp_right r).comp_left l = B.comp l r

@[simp]
theorem bilin_form.comp_apply {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {N : Type w} [add_comm_group N] [module R N] (B : bilin_form R N) (l r : M →ₗ[R] N) (v w : M) :
(B.comp l r) v w = B (l v) (r w)

@[simp]
theorem bilin_form.comp_left_apply {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] (B : bilin_form R M) (f : M →ₗ[R] M) (v w : M) :
(B.comp_left f) v w = B (f v) w

@[simp]
theorem bilin_form.comp_right_apply {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] (B : bilin_form R M) (f : M →ₗ[R] M) (v w : M) :
(B.comp_right f) v w = B v (f w)

theorem bilin_form.comp_injective {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {N : Type w} [add_comm_group N] [module R N] (B₁ B₂ : bilin_form R N) (l r : M →ₗ[R] N) :
function.surjective lfunction.surjective r(B₁.comp l r = B₂.comp l r B₁ = B₂)

def bilin_form.lin_mul_lin {M : Type v} [add_comm_group M] {R₂ : Type u_1} [comm_ring R₂] [module R₂ M] :
(M →ₗ[R₂] R₂)(M →ₗ[R₂] R₂)bilin_form R₂ M

lin_mul_lin f g is the bilinear form mapping x and y to f x * g y

Equations
@[simp]
theorem bilin_form.lin_mul_lin_apply {M : Type v} [add_comm_group M] {R₂ : Type u_1} [comm_ring R₂] [module R₂ M] {f g : M →ₗ[R₂] R₂} (x y : M) :
(bilin_form.lin_mul_lin f g) x y = (f x) * g y

@[simp]
theorem bilin_form.lin_mul_lin_comp {M : Type v} [add_comm_group M] {R₂ : Type u_1} [comm_ring R₂] [module R₂ M] {N : Type w} [add_comm_group N] [module R₂ N] {f g : M →ₗ[R₂] R₂} (l r : N →ₗ[R₂] M) :

@[simp]
theorem bilin_form.lin_mul_lin_comp_left {M : Type v} [add_comm_group M] {R₂ : Type u_1} [comm_ring R₂] [module R₂ M] {f g : M →ₗ[R₂] R₂} (l : M →ₗ[R₂] M) :

@[simp]
theorem bilin_form.lin_mul_lin_comp_right {M : Type v} [add_comm_group M] {R₂ : Type u_1} [comm_ring R₂] [module R₂ M] {f g : M →ₗ[R₂] R₂} (r : M →ₗ[R₂] M) :

def bilin_form.is_ortho {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] :
bilin_form R MM → M → Prop

The proposition that two elements of a bilinear form space are orthogonal

Equations
theorem bilin_form.ortho_zero {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {B : bilin_form R M} (x : M) :
B.is_ortho 0 x

theorem bilin_form.ortho_smul_left {M : Type v} [add_comm_group M] {R₃ : Type u_1} [domain R₃] [module R₃ M] {G : bilin_form R₃ M} {x y : M} {a : R₃} :
a 0(G.is_ortho x y G.is_ortho (a x) y)

theorem bilin_form.ortho_smul_right {M : Type v} [add_comm_group M] {R₃ : Type u_1} [domain R₃] [module R₃ M] {G : bilin_form R₃ M} {x y : M} {a : R₃} :
a 0(G.is_ortho x y G.is_ortho x (a y))

def matrix.to_bilin_formₗ {R : Type u} [comm_ring R] {n : Type u_1} [fintype n] :
matrix n n R →ₗ[R] bilin_form R (n → R)

The linear map from matrix n n R to bilinear forms on n → R.

Equations
def matrix.to_bilin_form {R : Type u} [comm_ring R] {n : Type u_1} [fintype n] :
matrix n n Rbilin_form R (n → R)

The map from matrix n n R to bilinear forms on n → R.

Equations
theorem matrix.to_bilin_form_apply {R : Type u} [comm_ring R] {n : Type u_1} [fintype n] (M : matrix n n R) (v w : n → R) :

def bilin_form.to_matrixₗ {R : Type u} [comm_ring R] {n : Type u_1} [fintype n] [decidable_eq n] :
bilin_form R (n → R) →ₗ[R] matrix n n R

The linear map from bilinear forms on n → R to matrix n n R.

Equations
def bilin_form.to_matrix {R : Type u} [comm_ring R] {n : Type u_1} [fintype n] [decidable_eq n] :
bilin_form R (n → R)matrix n n R

The map from bilinear forms on n → R to matrix n n R.

Equations
theorem bilin_form.to_matrix_apply {R : Type u} [comm_ring R] {n : Type u_1} [fintype n] [decidable_eq n] (B : bilin_form R (n → R)) (i j : n) :
B.to_matrix i j = B (λ (n_1 : n), ite (n_1 = i) 1 0) (λ (n_1 : n), ite (n_1 = j) 1 0)

theorem bilin_form.to_matrix_smul {R : Type u} [comm_ring R] {n : Type u_1} [fintype n] [decidable_eq n] (B : bilin_form R (n → R)) (x : R) :

theorem bilin_form.to_matrix_comp {R : Type u} [comm_ring R] {n : Type u_1} {o : Type u_2} [fintype n] [fintype o] [decidable_eq n] [decidable_eq o] (B : bilin_form R (n → R)) (l r : (o → R) →ₗ[R] n → R) :

theorem bilin_form.to_matrix_comp_left {R : Type u} [comm_ring R] {n : Type u_1} [fintype n] [decidable_eq n] (B : bilin_form R (n → R)) (f : (n → R) →ₗ[R] n → R) :

theorem bilin_form.to_matrix_comp_right {R : Type u} [comm_ring R] {n : Type u_1} [fintype n] [decidable_eq n] (B : bilin_form R (n → R)) (f : (n → R) →ₗ[R] n → R) :

theorem bilin_form.mul_to_matrix_mul {R : Type u} [comm_ring R] {n : Type u_1} {o : Type u_2} [fintype n] [fintype o] [decidable_eq n] [decidable_eq o] (B : bilin_form R (n → R)) (M : matrix o n R) (N : matrix n o R) :

theorem bilin_form.mul_to_matrix {R : Type u} [comm_ring R] {n : Type u_1} [fintype n] [decidable_eq n] (B : bilin_form R (n → R)) (M : matrix n n R) :

theorem bilin_form.to_matrix_mul {R : Type u} [comm_ring R] {n : Type u_1} [fintype n] [decidable_eq n] (B : bilin_form R (n → R)) (M : matrix n n R) :

@[simp]
theorem to_matrix_to_bilin_form {R : Type u} [comm_ring R] {n : Type u_1} [fintype n] [decidable_eq n] (B : bilin_form R (n → R)) :

@[simp]
theorem to_bilin_form_to_matrix {R : Type u} [comm_ring R] {n : Type u_1} [fintype n] [decidable_eq n] (M : matrix n n R) :

def bilin_form_equiv_matrix {R : Type u} [comm_ring R] {n : Type u_1} [fintype n] [decidable_eq n] :
bilin_form R (n → R) ≃ₗ[R] matrix n n R

Bilinear forms are linearly equivalent to matrices.

Equations
theorem matrix.to_bilin_form_comp {R : Type u} [comm_ring R] {n o : Type w} [fintype n] [fintype o] [decidable_eq o] (M : matrix n n R) (P Q : matrix n o R) :

def refl_bilin_form.is_refl {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] :
bilin_form R M → Prop

The proposition that a bilinear form is reflexive

Equations
theorem refl_bilin_form.eq_zero {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] {B : bilin_form R M} (H : refl_bilin_form.is_refl B) {x y : M} :
B x y = 0B y x = 0

theorem refl_bilin_form.ortho_sym {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] {B : bilin_form R M} (H : refl_bilin_form.is_refl B) {x y : M} :
B.is_ortho x y B.is_ortho y x

def sym_bilin_form.is_sym {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] :
bilin_form R M → Prop

The proposition that a bilinear form is symmetric

Equations
theorem sym_bilin_form.sym {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] {B : bilin_form R M} (H : sym_bilin_form.is_sym B) (x y : M) :
B x y = B y x

theorem sym_bilin_form.is_refl {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] {B : bilin_form R M} :

theorem sym_bilin_form.ortho_sym {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] {B : bilin_form R M} (H : sym_bilin_form.is_sym B) {x y : M} :
B.is_ortho x y B.is_ortho y x

def alt_bilin_form.is_alt {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] :
bilin_form R M → Prop

The proposition that a bilinear form is alternating

Equations
theorem alt_bilin_form.self_eq_zero {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] {B : bilin_form R M} (H : alt_bilin_form.is_alt B) (x : M) :
B x x = 0

theorem alt_bilin_form.neg {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] {B : bilin_form R M} (H : alt_bilin_form.is_alt B) (x y : M) :
-B x y = B y x

def bilin_form.is_adjoint_pair {R : Type u} [comm_ring R] {M : Type v} [add_comm_group M] [module R M] {M₂ : Type w} [add_comm_group M₂] [module R M₂] :
bilin_form R Mbilin_form R M₂(M →ₗ[R] M₂)(M₂ →ₗ[R] M) → Prop

Given a pair of modules equipped with bilinear forms, this is the condition for a pair of maps between them to be mutually adjoint.

Equations
theorem bilin_form.is_adjoint_pair.eq {R : Type u} [comm_ring R] {M : Type v} [add_comm_group M] [module R M] {M₂ : Type w} [add_comm_group M₂] [module R M₂] {B : bilin_form R M} {B₂ : bilin_form R M₂} {f : M →ₗ[R] M₂} {g : M₂ →ₗ[R] M} (h : B.is_adjoint_pair B₂ f g) {x : M} {y : M₂} :
B₂ (f x) y = B x (g y)

theorem bilin_form.is_adjoint_pair_iff_comp_left_eq_comp_right {R : Type u} [comm_ring R] {M : Type v} [add_comm_group M] [module R M] {B B' : bilin_form R M} (f g : module.End R M) :

theorem bilin_form.is_adjoint_pair_zero {R : Type u} [comm_ring R] {M : Type v} [add_comm_group M] [module R M] {M₂ : Type w} [add_comm_group M₂] [module R M₂] {B : bilin_form R M} {B₂ : bilin_form R M₂} :
B.is_adjoint_pair B₂ 0 0

theorem bilin_form.is_adjoint_pair_id {R : Type u} [comm_ring R] {M : Type v} [add_comm_group M] [module R M] {B : bilin_form R M} :

theorem bilin_form.is_adjoint_pair.add {R : Type u} [comm_ring R] {M : Type v} [add_comm_group M] [module R M] {M₂ : Type w} [add_comm_group M₂] [module R M₂] {B : bilin_form R M} {B₂ : bilin_form R M₂} {f f' : M →ₗ[R] M₂} {g g' : M₂ →ₗ[R] M} :
B.is_adjoint_pair B₂ f gB.is_adjoint_pair B₂ f' g'B.is_adjoint_pair B₂ (f + f') (g + g')

theorem bilin_form.is_adjoint_pair.sub {R : Type u} [comm_ring R] {M : Type v} [add_comm_group M] [module R M] {M₂ : Type w} [add_comm_group M₂] [module R M₂] {B : bilin_form R M} {B₂ : bilin_form R M₂} {f f' : M →ₗ[R] M₂} {g g' : M₂ →ₗ[R] M} :
B.is_adjoint_pair B₂ f gB.is_adjoint_pair B₂ f' g'B.is_adjoint_pair B₂ (f - f') (g - g')

theorem bilin_form.is_adjoint_pair.smul {R : Type u} [comm_ring R] {M : Type v} [add_comm_group M] [module R M] {M₂ : Type w} [add_comm_group M₂] [module R M₂] {B : bilin_form R M} {B₂ : bilin_form R M₂} {f : M →ₗ[R] M₂} {g : M₂ →ₗ[R] M} (c : R) :
B.is_adjoint_pair B₂ f gB.is_adjoint_pair B₂ (c f) (c g)

theorem bilin_form.is_adjoint_pair.comp {R : Type u} [comm_ring R] {M : Type v} [add_comm_group M] [module R M] {M₂ : Type w} [add_comm_group M₂] [module R M₂] {B : bilin_form R M} {B₂ : bilin_form R M₂} {f : M →ₗ[R] M₂} {g : M₂ →ₗ[R] M} {M₃ : Type v} [add_comm_group M₃] [module R M₃] {B₃ : bilin_form R M₃} {f' : M₂ →ₗ[R] M₃} {g' : M₃ →ₗ[R] M₂} :
B.is_adjoint_pair B₂ f gB₂.is_adjoint_pair B₃ f' g'B.is_adjoint_pair B₃ (f'.comp f) (g.comp g')

theorem bilin_form.is_adjoint_pair.mul {R : Type u} [comm_ring R] {M : Type v} [add_comm_group M] [module R M] {B : bilin_form R M} {f g f' g' : module.End R M} :
B.is_adjoint_pair B f gB.is_adjoint_pair B f' g'B.is_adjoint_pair B (f * f') (g' * g)

def bilin_form.is_pair_self_adjoint {R : Type u} [comm_ring R] {M : Type v} [add_comm_group M] [module R M] :
bilin_form R Mbilin_form R Mmodule.End R M → Prop

The condition for an endomorphism to be "self-adjoint" with respect to a pair of bilinear forms on the underlying module. In the case that these two forms are identical, this is the usual concept of self adjointness. In the case that one of the forms is the negation of the other, this is the usual concept of skew adjointness.

Equations
def bilin_form.is_pair_self_adjoint_submodule {R : Type u} [comm_ring R] {M : Type v} [add_comm_group M] [module R M] :
bilin_form R Mbilin_form R Msubmodule R (module.End R M)

The set of pair-self-adjoint endomorphisms are a submodule of the type of all endomorphisms.

Equations
@[simp]

theorem bilin_form.is_pair_self_adjoint_equiv {R : Type u} [comm_ring R] {M : Type v} [add_comm_group M] [module R M] {M₂ : Type w} [add_comm_group M₂] [module R M₂] (B B' : bilin_form R M) (e : M₂ ≃ₗ[R] M) (f : module.End R M) :

def bilin_form.is_self_adjoint {R : Type u} [comm_ring R] {M : Type v} [add_comm_group M] [module R M] :
bilin_form R Mmodule.End R M → Prop

An endomorphism of a module is self-adjoint with respect to a bilinear form if it serves as an adjoint for itself.

Equations
def bilin_form.is_skew_adjoint {R : Type u} [comm_ring R] {M : Type v} [add_comm_group M] [module R M] :
bilin_form R Mmodule.End R M → Prop

An endomorphism of a module is skew-adjoint with respect to a bilinear form if its negation serves as an adjoint.

Equations
theorem bilin_form.is_skew_adjoint_iff_neg_self_adjoint {R : Type u} [comm_ring R] {M : Type v} [add_comm_group M] [module R M] (B : bilin_form R M) (f : module.End R M) :

def bilin_form.self_adjoint_submodule {R : Type u} [comm_ring R] {M : Type v} [add_comm_group M] [module R M] :

The set of self-adjoint endomorphisms of a module with bilinear form is a submodule. (In fact it is a Jordan subalgebra.)

Equations
@[simp]
theorem bilin_form.mem_self_adjoint_submodule {R : Type u} [comm_ring R] {M : Type v} [add_comm_group M] [module R M] (B : bilin_form R M) (f : module.End R M) :

def bilin_form.skew_adjoint_submodule {R : Type u} [comm_ring R] {M : Type v} [add_comm_group M] [module R M] :

The set of skew-adjoint endomorphisms of a module with bilinear form is a submodule. (In fact it is a Lie subalgebra.)

Equations
@[simp]
theorem bilin_form.mem_skew_adjoint_submodule {R : Type u} [comm_ring R] {M : Type v} [add_comm_group M] [module R M] (B : bilin_form R M) (f : module.End R M) :

def matrix.is_adjoint_pair {R : Type u} [comm_ring R] {n : Type w} [fintype n] :
matrix n n Rmatrix n n Rmatrix n n Rmatrix n n R → Prop

The condition for the square matrices A, B to be an adjoint pair with respect to the square matrices J, J₂.

Equations
def matrix.is_self_adjoint {R : Type u} [comm_ring R] {n : Type w} [fintype n] :
matrix n n Rmatrix n n R → Prop

The condition for a square matrix A to be self-adjoint with respect to the square matrix J.

Equations
def matrix.is_skew_adjoint {R : Type u} [comm_ring R] {n : Type w} [fintype n] :
matrix n n Rmatrix n n R → Prop

The condition for a square matrix A to be skew-adjoint with respect to the square matrix J.

Equations
@[simp]
theorem matrix_is_adjoint_pair_bilin_form {R : Type u} [comm_ring R] {n : Type w} [fintype n] (J J₂ A B : matrix n n R) [decidable_eq n] :

theorem matrix.is_adjoint_pair_equiv {R : Type u} [comm_ring R] {n : Type w} [fintype n] (J A B : matrix n n R) [decidable_eq n] (P : matrix n n R) :
is_unit P((P J P).is_adjoint_pair (P J P) A B J.is_adjoint_pair J (P A P⁻¹) (P B P⁻¹))

def pair_self_adjoint_matrices_submodule {R : Type u} [comm_ring R] {n : Type w} [fintype n] (J J₂ : matrix n n R) [decidable_eq n] :
submodule R (matrix n n R)

The submodule of pair-self-adjoint matrices with respect to bilinear forms corresponding to given matrices J, J₂.

Equations
@[simp]
theorem mem_pair_self_adjoint_matrices_submodule {R : Type u} [comm_ring R] {n : Type w} [fintype n] (J J₂ A : matrix n n R) [decidable_eq n] :

def self_adjoint_matrices_submodule {R : Type u} [comm_ring R] {n : Type w} [fintype n] (J : matrix n n R) [decidable_eq n] :
submodule R (matrix n n R)

The submodule of self-adjoint matrices with respect to the bilinear form corresponding to the matrix J.

Equations
@[simp]
theorem mem_self_adjoint_matrices_submodule {R : Type u} [comm_ring R] {n : Type w} [fintype n] (J A : matrix n n R) [decidable_eq n] :

def skew_adjoint_matrices_submodule {R : Type u} [comm_ring R] {n : Type w} [fintype n] (J : matrix n n R) [decidable_eq n] :
submodule R (matrix n n R)

The submodule of skew-adjoint matrices with respect to the bilinear form corresponding to the matrix J.

Equations
@[simp]
theorem mem_skew_adjoint_matrices_submodule {R : Type u} [comm_ring R] {n : Type w} [fintype n] (J A : matrix n n R) [decidable_eq n] :