Commit 2023-06-06 10:51 6f0499b5

View on Github →

feat: port LinearAlgebra.QuadraticForm.Isometry (#4703)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/QuadraticForm/Isometry.lean

added theorem QuadraticForm.Equivalent.refl

added theorem QuadraticForm.Equivalent.symm

added theorem QuadraticForm.Equivalent.trans

added def QuadraticForm.Equivalent

added theorem QuadraticForm.Isometry.coe_toLinearEquiv

added theorem QuadraticForm.Isometry.map_app

added def QuadraticForm.Isometry.refl

added def QuadraticForm.Isometry.symm

added def QuadraticForm.Isometry.trans

added structure QuadraticForm.Isometry

added theorem QuadraticForm.equivalent_weightedSumSquares

added theorem QuadraticForm.equivalent_weightedSumSquares_units_of_nondegenerate'

added def QuadraticForm.isometryOfCompLinearEquiv