Documentation

Mathlib.LinearAlgebra.BilinearForm.Properties

Bilinear form #

This file defines various properties of bilinear forms, including reflexivity, symmetry, alternativity, adjoint, and non-degeneracy. For orthogonality, see LinearAlgebra/BilinearForm/Orthogonal.lean.

Notations #

Given any term B of type BilinForm, 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.

In this file we use the following type variables:

References #

Tags #

Bilinear form,

Reflexivity, symmetry, and alternativity #

The proposition that a bilinear form is reflexive

Equations
Instances For
    theorem LinearMap.BilinForm.IsRefl.eq_zero {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} (H : B.IsRefl) {x : M} {y : M} :
    (B x) y = 0(B y) x = 0
    theorem LinearMap.BilinForm.IsRefl.neg {R₁ : Type u_3} {M₁ : Type u_4} [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] {B : LinearMap.BilinForm R₁ M₁} (hB : B.IsRefl) :
    (-B).IsRefl
    theorem LinearMap.BilinForm.IsRefl.smul {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {α : Type u_9} [CommSemiring α] [Module α R] [SMulCommClass R α R] [NoZeroSMulDivisors α R] (a : α) {B : LinearMap.BilinForm R M} (hB : B.IsRefl) :
    (a B).IsRefl
    theorem LinearMap.BilinForm.IsRefl.groupSMul {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {α : Type u_9} [Group α] [DistribMulAction α R] [SMulCommClass R α R] (a : α) {B : LinearMap.BilinForm R M} (hB : B.IsRefl) :
    (a B).IsRefl
    @[simp]
    theorem LinearMap.BilinForm.isRefl_neg {R₁ : Type u_3} {M₁ : Type u_4} [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] {B : LinearMap.BilinForm R₁ M₁} :
    (-B).IsRefl B.IsRefl

    The proposition that a bilinear form is symmetric

    Equations
    Instances For
      theorem LinearMap.BilinForm.IsSymm.eq {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} (H : B.IsSymm) (x : M) (y : M) :
      (B x) y = (B y) x
      theorem LinearMap.BilinForm.IsSymm.isRefl {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} (H : B.IsSymm) :
      B.IsRefl
      theorem LinearMap.BilinForm.IsSymm.add {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B₁ : LinearMap.BilinForm R M} {B₂ : LinearMap.BilinForm R M} (hB₁ : B₁.IsSymm) (hB₂ : B₂.IsSymm) :
      (B₁ + B₂).IsSymm
      theorem LinearMap.BilinForm.IsSymm.sub {R₁ : Type u_3} {M₁ : Type u_4} [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] {B₁ : LinearMap.BilinForm R₁ M₁} {B₂ : LinearMap.BilinForm R₁ M₁} (hB₁ : B₁.IsSymm) (hB₂ : B₂.IsSymm) :
      (B₁ - B₂).IsSymm
      theorem LinearMap.BilinForm.IsSymm.neg {R₁ : Type u_3} {M₁ : Type u_4} [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] {B : LinearMap.BilinForm R₁ M₁} (hB : B.IsSymm) :
      (-B).IsSymm
      theorem LinearMap.BilinForm.IsSymm.smul {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {α : Type u_9} [Monoid α] [DistribMulAction α R] [SMulCommClass R α R] (a : α) {B : LinearMap.BilinForm R M} (hB : B.IsSymm) :
      (a B).IsSymm
      theorem LinearMap.BilinForm.IsSymm.restrict {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} (b : B.IsSymm) (W : Submodule R M) :
      (B.restrict W).IsSymm

      The restriction of a symmetric bilinear form on a submodule is also symmetric.

      @[simp]
      theorem LinearMap.BilinForm.isSymm_neg {R₁ : Type u_3} {M₁ : Type u_4} [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] {B : LinearMap.BilinForm R₁ M₁} :
      (-B).IsSymm B.IsSymm
      theorem LinearMap.BilinForm.isSymm_iff_flip {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} :
      B.IsSymm LinearMap.BilinForm.flipHom B = B

      The proposition that a bilinear form is alternating

      Equations
      Instances For
        theorem LinearMap.BilinForm.IsAlt.self_eq_zero {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} (H : B.IsAlt) (x : M) :
        (B x) x = 0
        theorem LinearMap.BilinForm.IsAlt.neg_eq {R₁ : Type u_3} {M₁ : Type u_4} [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] {B₁ : LinearMap.BilinForm R₁ M₁} (H : B₁.IsAlt) (x : M₁) (y : M₁) :
        -(B₁ x) y = (B₁ y) x
        theorem LinearMap.BilinForm.IsAlt.isRefl {R₁ : Type u_3} {M₁ : Type u_4} [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] {B₁ : LinearMap.BilinForm R₁ M₁} (H : B₁.IsAlt) :
        B₁.IsRefl
        theorem LinearMap.BilinForm.IsAlt.eq_of_add_add_eq_zero {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} [IsCancelAdd R] {a : M} {b : M} {c : M} (H : B.IsAlt) (hAdd : a + b + c = 0) :
        (B a) b = (B b) c
        theorem LinearMap.BilinForm.IsAlt.add {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B₁ : LinearMap.BilinForm R M} {B₂ : LinearMap.BilinForm R M} (hB₁ : B₁.IsAlt) (hB₂ : B₂.IsAlt) :
        (B₁ + B₂).IsAlt
        theorem LinearMap.BilinForm.IsAlt.sub {R₁ : Type u_3} {M₁ : Type u_4} [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] {B₁ : LinearMap.BilinForm R₁ M₁} {B₂ : LinearMap.BilinForm R₁ M₁} (hB₁ : B₁.IsAlt) (hB₂ : B₂.IsAlt) :
        (B₁ - B₂).IsAlt
        theorem LinearMap.BilinForm.IsAlt.neg {R₁ : Type u_3} {M₁ : Type u_4} [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] {B : LinearMap.BilinForm R₁ M₁} (hB : B.IsAlt) :
        (-B).IsAlt
        theorem LinearMap.BilinForm.IsAlt.smul {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {α : Type u_9} [Monoid α] [DistribMulAction α R] [SMulCommClass R α R] (a : α) {B : LinearMap.BilinForm R M} (hB : B.IsAlt) :
        (a B).IsAlt
        @[simp]
        theorem LinearMap.BilinForm.isAlt_neg {R₁ : Type u_3} {M₁ : Type u_4} [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] {B : LinearMap.BilinForm R₁ M₁} :
        (-B).IsAlt B.IsAlt

        Linear adjoints #

        def LinearMap.BilinForm.IsAdjointPair {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) {M' : Type u_9} [AddCommMonoid M'] [Module R M'] (B' : LinearMap.BilinForm R M') (f : M →ₗ[R] M') (g : M' →ₗ[R] M) :

        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
        • B.IsAdjointPair B' f g = ∀ ⦃x : M⦄ ⦃y : M'⦄, (B' (f x)) y = (B x) (g y)
        Instances For
          theorem LinearMap.BilinForm.IsAdjointPair.eq {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {M' : Type u_9} [AddCommMonoid M'] [Module R M'] {B' : LinearMap.BilinForm R M'} {f : M →ₗ[R] M'} {g : M' →ₗ[R] M} (h : B.IsAdjointPair B' f g) {x : M} {y : M'} :
          (B' (f x)) y = (B x) (g y)
          theorem LinearMap.BilinForm.isAdjointPair_iff_compLeft_eq_compRight {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} (F : LinearMap.BilinForm R M) (f : Module.End R M) (g : Module.End R M) :
          B.IsAdjointPair F f g F.compLeft f = B.compRight g
          theorem LinearMap.BilinForm.isAdjointPair_zero {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {M' : Type u_9} [AddCommMonoid M'] [Module R M'] {B' : LinearMap.BilinForm R M'} :
          B.IsAdjointPair B' 0 0
          theorem LinearMap.BilinForm.isAdjointPair_id {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} :
          B.IsAdjointPair B 1 1
          theorem LinearMap.BilinForm.IsAdjointPair.add {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {M' : Type u_9} [AddCommMonoid M'] [Module R M'] {B' : LinearMap.BilinForm R M'} {f : M →ₗ[R] M'} {f' : M →ₗ[R] M'} {g : M' →ₗ[R] M} {g' : M' →ₗ[R] M} (h : B.IsAdjointPair B' f g) (h' : B.IsAdjointPair B' f' g') :
          B.IsAdjointPair B' (f + f') (g + g')
          theorem LinearMap.BilinForm.IsAdjointPair.sub {R₁ : Type u_3} {M₁ : Type u_4} [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] {B₁ : LinearMap.BilinForm R₁ M₁} {M₁' : Type u_10} [AddCommGroup M₁'] [Module R₁ M₁'] {B₁' : LinearMap.BilinForm R₁ M₁'} {f₁ : M₁ →ₗ[R₁] M₁'} {f₁' : M₁ →ₗ[R₁] M₁'} {g₁ : M₁' →ₗ[R₁] M₁} {g₁' : M₁' →ₗ[R₁] M₁} (h : B₁.IsAdjointPair B₁' f₁ g₁) (h' : B₁.IsAdjointPair B₁' f₁' g₁') :
          B₁.IsAdjointPair B₁' (f₁ - f₁') (g₁ - g₁')
          theorem LinearMap.BilinForm.IsAdjointPair.smul {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {M' : Type u_9} [AddCommMonoid M'] [Module R M'] {B₂' : LinearMap.BilinForm R M'} {f₂ : M →ₗ[R] M'} {g₂ : M' →ₗ[R] M} (c : R) (h : B.IsAdjointPair B₂' f₂ g₂) :
          B.IsAdjointPair B₂' (c f₂) (c g₂)
          theorem LinearMap.BilinForm.IsAdjointPair.comp {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {M' : Type u_9} [AddCommMonoid M'] [Module R M'] {B' : LinearMap.BilinForm R M'} {f : M →ₗ[R] M'} {g : M' →ₗ[R] M} {M'' : Type u_11} [AddCommMonoid M''] [Module R M''] (B'' : LinearMap.BilinForm R M'') {f' : M' →ₗ[R] M''} {g' : M'' →ₗ[R] M'} (h : B.IsAdjointPair B' f g) (h' : B'.IsAdjointPair B'' f' g') :
          B.IsAdjointPair B'' (f' ∘ₗ f) (g ∘ₗ g')
          theorem LinearMap.BilinForm.IsAdjointPair.mul {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {f : Module.End R M} {g : Module.End R M} {f' : Module.End R M} {g' : Module.End R M} (h : B.IsAdjointPair B f g) (h' : B.IsAdjointPair B f' g') :
          B.IsAdjointPair B (f * f') (g' * g)

          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
          • B.IsPairSelfAdjoint F f = B.IsAdjointPair F f f
          Instances For

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

            Equations
            • B₂.isPairSelfAdjointSubmodule F₂ = { carrier := {f : Module.End R M | B₂.IsPairSelfAdjoint F₂ f}, add_mem' := , zero_mem' := , smul_mem' := }
            Instances For
              @[simp]
              theorem LinearMap.BilinForm.mem_isPairSelfAdjointSubmodule {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B₂ : LinearMap.BilinForm R M) (F₂ : LinearMap.BilinForm R M) (f : Module.End R M) :
              f B₂.isPairSelfAdjointSubmodule F₂ B₂.IsPairSelfAdjoint F₂ f
              theorem LinearMap.BilinForm.isPairSelfAdjoint_equiv {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {M' : Type u_9} [AddCommMonoid M'] [Module R M'] (B₂ : LinearMap.BilinForm R M) (F₂ : LinearMap.BilinForm R M) (e : M' ≃ₗ[R] M) (f : Module.End R M) :
              B₂.IsPairSelfAdjoint F₂ f (B₂.comp e e).IsPairSelfAdjoint (F₂.comp e e) (e.symm.conj f)

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

              Equations
              • B.IsSelfAdjoint f = B.IsAdjointPair B f f
              Instances For
                def LinearMap.BilinForm.IsSkewAdjoint {R₁ : Type u_3} {M₁ : Type u_4} [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] (B₁ : LinearMap.BilinForm R₁ M₁) (f : Module.End R₁ M₁) :

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

                Equations
                • B₁.IsSkewAdjoint f = B₁.IsAdjointPair B₁ f (-f)
                Instances For
                  theorem LinearMap.BilinForm.isSkewAdjoint_iff_neg_self_adjoint {R₁ : Type u_3} {M₁ : Type u_4} [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] (B₁ : LinearMap.BilinForm R₁ M₁) (f : Module.End R₁ M₁) :
                  B₁.IsSkewAdjoint f (-B₁).IsAdjointPair B₁ f f

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

                  Equations
                  • B.selfAdjointSubmodule = B.isPairSelfAdjointSubmodule B
                  Instances For
                    @[simp]
                    theorem LinearMap.BilinForm.mem_selfAdjointSubmodule {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) (f : Module.End R M) :
                    f B.selfAdjointSubmodule B.IsSelfAdjoint f
                    def LinearMap.BilinForm.skewAdjointSubmodule {R₁ : Type u_3} {M₁ : Type u_4} [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] (B₁ : LinearMap.BilinForm R₁ M₁) :
                    Submodule R₁ (Module.End 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
                    • B₁.skewAdjointSubmodule = (-B₁).isPairSelfAdjointSubmodule B₁
                    Instances For
                      @[simp]
                      theorem LinearMap.BilinForm.mem_skewAdjointSubmodule {R₁ : Type u_3} {M₁ : Type u_4} [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] (B₁ : LinearMap.BilinForm R₁ M₁) (f : Module.End R₁ M₁) :
                      f B₁.skewAdjointSubmodule B₁.IsSkewAdjoint f

                      A nondegenerate bilinear form is a bilinear form such that the only element that is orthogonal to every other element is 0; i.e., for all nonzero m in M, there exists n in M with B m n ≠ 0.

                      Note that for general (neither symmetric nor antisymmetric) bilinear forms this definition has a chirality; in addition to this "left" nondegeneracy condition one could define a "right" nondegeneracy condition that in the situation described, B n m ≠ 0. This variant definition is not currently provided in mathlib. In finite dimension either definition implies the other.

                      Equations
                      • B.Nondegenerate = ∀ (m : M), (∀ (n : M), (B m) n = 0)m = 0
                      Instances For

                        In a non-trivial module, zero is not non-degenerate.

                        theorem LinearMap.BilinForm.Nondegenerate.ne_zero {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] [Nontrivial M] {B : LinearMap.BilinForm R M} (h : B.Nondegenerate) :
                        B 0
                        theorem LinearMap.BilinForm.Nondegenerate.congr {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {M' : Type u_9} [AddCommMonoid M'] [Module R M'] {B : LinearMap.BilinForm R M} (e : M ≃ₗ[R] M') (h : B.Nondegenerate) :
                        ((LinearMap.BilinForm.congr e) B).Nondegenerate
                        @[simp]
                        theorem LinearMap.BilinForm.nondegenerate_congr_iff {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {M' : Type u_9} [AddCommMonoid M'] [Module R M'] {B : LinearMap.BilinForm R M} (e : M ≃ₗ[R] M') :
                        ((LinearMap.BilinForm.congr e) B).Nondegenerate B.Nondegenerate

                        A bilinear form is nondegenerate if and only if it has a trivial kernel.

                        theorem LinearMap.BilinForm.Nondegenerate.ker_eq_bot {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} (h : B.Nondegenerate) :
                        theorem LinearMap.BilinForm.compLeft_injective {R₁ : Type u_3} {M₁ : Type u_4} [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] (B : LinearMap.BilinForm R₁ M₁) (b : B.Nondegenerate) :
                        theorem LinearMap.BilinForm.isAdjointPair_unique_of_nondegenerate {R₁ : Type u_3} {M₁ : Type u_4} [CommRing R₁] [AddCommGroup M₁] [Module R₁ M₁] (B : LinearMap.BilinForm R₁ M₁) (b : B.Nondegenerate) (φ : M₁ →ₗ[R₁] M₁) (ψ₁ : M₁ →ₗ[R₁] M₁) (ψ₂ : M₁ →ₗ[R₁] M₁) (hψ₁ : B.IsAdjointPair B ψ₁ φ) (hψ₂ : B.IsAdjointPair B ψ₂ φ) :
                        ψ₁ = ψ₂
                        noncomputable def LinearMap.BilinForm.toDual {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (B : LinearMap.BilinForm K V) (b : B.Nondegenerate) :

                        Given a nondegenerate bilinear form B on a finite-dimensional vector space, B.toDual is the linear equivalence between a vector space and its dual.

                        Equations
                        Instances For
                          theorem LinearMap.BilinForm.toDual_def {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {B : LinearMap.BilinForm K V} (b : LinearMap.SeparatingLeft B) {m : V} {n : V} :
                          ((B.toDual b) m) n = (B m) n
                          @[simp]
                          theorem LinearMap.BilinForm.apply_toDual_symm_apply {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {B : LinearMap.BilinForm K V} {hB : B.Nondegenerate} (f : Module.Dual K V) (v : V) :
                          (B ((B.toDual hB).symm f)) v = f v
                          theorem LinearMap.BilinForm.Nondegenerate.flip {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {B : LinearMap.BilinForm K V} (hB : B.Nondegenerate) :
                          B.flip.Nondegenerate
                          theorem LinearMap.BilinForm.nonDegenerateFlip_iff {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {B : LinearMap.BilinForm K V} :
                          B.flip.Nondegenerate B.Nondegenerate
                          noncomputable def LinearMap.BilinForm.dualBasis {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] {ι : Type u_10} [DecidableEq ι] [Finite ι] (B : LinearMap.BilinForm K V) (hB : B.Nondegenerate) (b : Basis ι K V) :
                          Basis ι K V

                          The B-dual basis B.dualBasis hB b to a finite basis b satisfies B (B.dualBasis hB b i) (b j) = B (b i) (B.dualBasis hB b j) = if i = j then 1 else 0, where B is a nondegenerate (symmetric) bilinear form and b is a finite basis.

                          Equations
                          • B.dualBasis hB b = b.dualBasis.map (B.toDual hB).symm
                          Instances For
                            @[simp]
                            theorem LinearMap.BilinForm.dualBasis_repr_apply {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] {ι : Type u_10} [DecidableEq ι] [Finite ι] (B : LinearMap.BilinForm K V) (hB : B.Nondegenerate) (b : Basis ι K V) (x : V) (i : ι) :
                            ((B.dualBasis hB b).repr x) i = (B x) (b i)
                            theorem LinearMap.BilinForm.apply_dualBasis_left {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] {ι : Type u_10} [DecidableEq ι] [Finite ι] (B : LinearMap.BilinForm K V) (hB : B.Nondegenerate) (b : Basis ι K V) (i : ι) (j : ι) :
                            (B ((B.dualBasis hB b) i)) (b j) = if j = i then 1 else 0
                            theorem LinearMap.BilinForm.apply_dualBasis_right {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] {ι : Type u_10} [DecidableEq ι] [Finite ι] (B : LinearMap.BilinForm K V) (hB : B.Nondegenerate) (sym : B.IsSymm) (b : Basis ι K V) (i : ι) (j : ι) :
                            (B (b i)) ((B.dualBasis hB b) j) = if i = j then 1 else 0
                            @[simp]
                            theorem LinearMap.BilinForm.dualBasis_dualBasis_flip {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (B : LinearMap.BilinForm K V) (hB : B.Nondegenerate) {ι : Type u_11} [Finite ι] [DecidableEq ι] (b : Basis ι K V) :
                            B.dualBasis hB (B.flip.dualBasis b) = b
                            @[simp]
                            theorem LinearMap.BilinForm.dualBasis_flip_dualBasis {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] (B : LinearMap.BilinForm K V) (hB : B.Nondegenerate) {ι : Type u_11} [Finite ι] [DecidableEq ι] [FiniteDimensional K V] (b : Basis ι K V) :
                            B.flip.dualBasis (B.dualBasis hB b) = b
                            @[simp]
                            theorem LinearMap.BilinForm.dualBasis_dualBasis {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] (B : LinearMap.BilinForm K V) (hB : B.Nondegenerate) (hB' : B.IsSymm) {ι : Type u_11} [Finite ι] [DecidableEq ι] [FiniteDimensional K V] (b : Basis ι K V) :
                            B.dualBasis hB (B.dualBasis hB b) = b
                            noncomputable def LinearMap.BilinForm.symmCompOfNondegenerate {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (B₁ : LinearMap.BilinForm K V) (B₂ : LinearMap.BilinForm K V) (b₂ : B₂.Nondegenerate) :

                            Given bilinear forms B₁, B₂ where B₂ is nondegenerate, symmCompOfNondegenerate is the linear map B₂ ∘ B₁.

                            Equations
                            • B₁.symmCompOfNondegenerate B₂ b₂ = (B₂.toDual b₂).symm ∘ₗ B₁
                            Instances For
                              theorem LinearMap.BilinForm.comp_symmCompOfNondegenerate_apply {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (B₁ : LinearMap.BilinForm K V) {B₂ : LinearMap.BilinForm K V} (b₂ : B₂.Nondegenerate) (v : V) :
                              B₂ ((B₁.symmCompOfNondegenerate B₂ b₂) v) = B₁ v
                              @[simp]
                              theorem LinearMap.BilinForm.symmCompOfNondegenerate_left_apply {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (B₁ : LinearMap.BilinForm K V) {B₂ : LinearMap.BilinForm K V} (b₂ : B₂.Nondegenerate) (v : V) (w : V) :
                              (B₂ ((B₁.symmCompOfNondegenerate B₂ b₂) w)) v = (B₁ w) v
                              noncomputable def LinearMap.BilinForm.leftAdjointOfNondegenerate {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (B : LinearMap.BilinForm K V) (b : B.Nondegenerate) (φ : V →ₗ[K] V) :

                              Given the nondegenerate bilinear form B and the linear map φ, leftAdjointOfNondegenerate provides the left adjoint of φ with respect to B. The lemma proving this property is BilinForm.isAdjointPairLeftAdjointOfNondegenerate.

                              Equations
                              • B.leftAdjointOfNondegenerate b φ = (B.compRight φ).symmCompOfNondegenerate B b
                              Instances For
                                theorem LinearMap.BilinForm.isAdjointPairLeftAdjointOfNondegenerate {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (B : LinearMap.BilinForm K V) (b : B.Nondegenerate) (φ : V →ₗ[K] V) :
                                B.IsAdjointPair B (B.leftAdjointOfNondegenerate b φ) φ
                                theorem LinearMap.BilinForm.isAdjointPair_iff_eq_of_nondegenerate {V : Type u_5} {K : Type u_6} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (B : LinearMap.BilinForm K V) (b : B.Nondegenerate) (ψ : V →ₗ[K] V) (φ : V →ₗ[K] V) :
                                B.IsAdjointPair B ψ φ ψ = B.leftAdjointOfNondegenerate b φ

                                Given the nondegenerate bilinear form B, the linear map φ has a unique left adjoint given by BilinForm.leftAdjointOfNondegenerate.