## Stream: maths

### Topic: nondegenerate bilinear form

#### Jason KY. (Mar 06 2021 at 17:59):

In PR #5814 I defined nondegenerate bilinear forms to be

def nondegenerate (B : bilin_form R M) : Prop :=
∀ m : M, (∀ n : M, B m n = 0) → m


As @Heather Macbeth pointed out this is not a symmetric definitionsince we can easily have defined it to be

def nondegenerate (B : bilin_form R M) : Prop :=
∀ m : M, (∀ n : M, B n m = 0) → m


Here (section 8.3) we have some definition of a symmetric version. Is this a better solution or should we keep it asymmetric as we have done for left cosets?

#### Heather Macbeth (Mar 06 2021 at 18:01):

Thank you for starting the discussion, Jason! Specifically, the lecture notes Jason linked are an example of someone choosing to define

def nondegenerate (B : bilin_form R M) : Prop :=
∀ m : M, ((∀ n : M, B m n = 0) → m = 0) ∧ ((∀ n : M, B n m = 0) → m = 0)


#### Heather Macbeth (Mar 06 2021 at 18:03):

(In finite dimension these definitions are all equivalent.)

#### Kevin Buzzard (Mar 06 2021 at 18:20):

Is this concept useful in the infinite-dimensional setting? I have only ever seen it being used in the finite-dimensional case in which case it doesn't matter

Last updated: May 14 2021 at 18:28 UTC