Commit 2023-06-16 07:08 74d091ea

View on Github →

feat: port Counterexamples.QuadraticForm (#5121)

Estimated changes

Modified Counterexamples.lean

Created Counterexamples/QuadraticForm.lean

added def Counterexample.B

added theorem Counterexample.B_apply

added theorem Counterexample.B_ne_zero

added theorem Counterexample.BilinForm.not_injOn_toQuadraticForm_isSymm.{u}

added theorem Counterexample.isAlt_B

added theorem Counterexample.isSymm_B